--- a/src/BAlgbra.agda	Mon Mar 14 17:51:16 2022 +0900
+++ b/src/BAlgbra.agda	Mon Mar 14 19:53:54 2022 +0900
@@ -50,6 +50,13 @@
 _＼_ : ( A B : HOD  ) → HOD
 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
 
+¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
+¬∅∋ {x} = ¬x<0
+
+[a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
+[a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
+     ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
+
 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
 ∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
     lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x