---

Step * of Lemma b-union-equality-disjoint2

∀A,B:Type. ∀a:A. ∀b:B.  ((a = b ∈ (A ⋃ B)) ⇒ (¬¬A ⋂ B))
BY
{ (InstLemma `b-union-equality-disjoint` [] THEN RepeatFor 4 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}a:A.  \mforall{}b:B.    ((a  =  b)  {}\mRightarrow{}  (\mneg{}\mneg{}A  \mcap{}  B))


By

---

Latex:
(InstLemma  `b-union-equality-disjoint`  []  THEN  RepeatFor  4  (ParallelLast)  THEN  Auto)

---

Home Index