---

Step * of Lemma geo-sep-O-X

∀e:EuclideanPlaneStructure. O ≠ X
BY
{ (Auto THEN Unfolds ``geo-O geo-X`` 0 THEN At ⌜Type⌝ (GenConclTerm ⌜geo-nontrivial(e)⌝)⋅ THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlaneStructure.  O  \mneq{}  X


By

---

Latex:
(Auto  THEN  Unfolds  ``geo-O  geo-X``  0  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (GenConclTerm  \mkleeneopen{}geo-nontrivial(e)\mkleeneclose{})\mcdot{}  THEN  Auto)

---

Home Index