---

Step * of Lemma geo-sep-exists

∀e:EuclideanPlane. ∀A:Point.  ∃A':Point. A ≠ A'
BY
{ (Auto THEN InstLemma `geo-sep-or` [⌜e⌝;⌜O⌝;⌜X⌝;⌜A⌝]⋅ THEN Auto) }

1
1. e : EuclideanPlane
2. A : Point
3. O ≠ A ∨ X ≠ A
⊢ ∃A':Point. A ≠ A'

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A:Point.    \mexists{}A':Point.  A  \mneq{}  A'


By

---

Latex:
(Auto  THEN  InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index