---

Step * 1 of Lemma geo-sep-exists


1. e : EuclideanPlane
2. A : Point
3. O ≠ A ∨ X ≠ A
⊢ ∃A':Point. A ≠ A'
BY
{ ((D -1 THENL [D 0 With ⌜O⌝ ; D 0 With ⌜X⌝ ]) THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  A  :  Point
3.  O  \mneq{}  A  \mvee{}  X  \mneq{}  A
\mvdash{}  \mexists{}A':Point.  A  \mneq{}  A'


By

---

Latex:
((D  -1  THENL  [D  0  With  \mkleeneopen{}O\mkleeneclose{}  ;  D  0  With  \mkleeneopen{}X\mkleeneclose{}  ])  THEN  Auto)

---

Home Index