---

Step * 1 of Lemma geo-sep-O-X


1. e : EuclideanPlaneStructure
2. v : ∃a:Point. (∃b:{Point| a ≠ b})
3. geo-nontrivial(e) = v ∈ (∃a:Point. (∃b:{Point| a ≠ b}))
⊢ fst(v) ≠ snd(v)
BY
{ ((D 2 THEN Reduce 0) THEN D -2 THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlaneStructure
2.  v  :  \mexists{}a:Point.  (\mexists{}b:\{Point|  a  \mneq{}  b\})
3.  geo-nontrivial(e)  =  v
\mvdash{}  fst(v)  \mneq{}  snd(v)


By

---

Latex:
((D  2  THEN  Reduce  0)  THEN  D  -2  THEN  Unhide  THEN  Auto)

---

Home Index