---

Step * of Lemma type-with-x=0-y=1

∀x,y:Base.  ∃T:Type. ((x = 0 ∈ T) ∧ (y = 1 ∈ T) ∧ ((0 = 1 ∈ T) ⇒ (↓(x = y ∈ Base) ∨ (x = 1 ∈ Base) ∨ (y = 0 ∈ Base))))
BY
{ (Auto
   THEN Assert ⌜EquivRel({z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} ;a,b.((x = y ∈ Base\000C)
                                                                                                ∨ (y = 0 ∈ Base)
                                                                                                ∨ (x = 1 ∈ Base))
                ∨ (a = b ∈ Base)
                ∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
                ∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
                ∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
                ∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base)))⌝⋅
   ) }

1
.....assertion..... 
1. x : Base
2. y : Base
⊢ EquivRel({z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} ;a,b.((x = y ∈ Base)
                                                                                ∨ (y = 0 ∈ Base)
                                                                                ∨ (x = 1 ∈ Base))
∨ (a = b ∈ Base)
∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base)))

2
1. x : Base
2. y : Base
3. EquivRel({z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} ;a,b.((x = y ∈ Base)
                                                                                ∨ (y = 0 ∈ Base)
                                                                                ∨ (x = 1 ∈ Base))
∨ (a = b ∈ Base)
∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base)))
⊢ ∃T:Type. ((x = 0 ∈ T) ∧ (y = 1 ∈ T) ∧ ((0 = 1 ∈ T) ⇒ (↓(x = y ∈ Base) ∨ (x = 1 ∈ Base) ∨ (y = 0 ∈ Base))))

---

Latex:

---

Latex:
\mforall{}x,y:Base.    \mexists{}T:Type.  ((x  =  0)  \mwedge{}  (y  =  1)  \mwedge{}  ((0  =  1)  {}\mRightarrow{}  (\mdownarrow{}(x  =  y)  \mvee{}  (x  =  1)  \mvee{}  (y  =  0))))


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}EquivRel(\{z:Base|  (z  =  0)  \mvee{}  (z  =  1)  \mvee{}  (z  =  x)  \mvee{}  (z  =  y)\}  ;a,b.((x  =  y)  \mvee{}  (y  =  0)  \mvee{}  (x  \000C=  1))
                            \mvee{}  (a  =  b)
                            \mvee{}  ((a  =  0)  \mwedge{}  (b  =  x))
                            \mvee{}  ((a  =  x)  \mwedge{}  (b  =  0))
                            \mvee{}  ((a  =  1)  \mwedge{}  (b  =  y))
                            \mvee{}  ((a  =  y)  \mwedge{}  (b  =  1)))\mkleeneclose{}\mcdot{}
  )

---

Home Index