---

Step * 1 1 of Lemma isect2-b-union-subtype

.....assertion..... 
1. A : Type
2. B : Type
3. C : Type
4. ¬B ⋂ C
5. x : A ⋂ B ⋃ C@i
⊢ ∃y:B ⋃ C. (y = x ∈ (B ⋃ C))
BY
{ (With ⌜x⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  \mneg{}B  \mcap{}  C
5.  x  :  A  \mcap{}  B  \mcup{}  C@i
\mvdash{}  \mexists{}y:B  \mcup{}  C.  (y  =  x)


By

---

Latex:
(With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index