---

Step * of Lemma geo-Op-sep

∀g:EuclideanPlane. ∀p:{p:Point| O_X_p} .  O ≠ p
BY
{ ((Auto THEN D -1 THEN Unhide THEN Auto) THEN FLemma `geo-between-sep` [-1]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}p:\{p:Point|  O\_X\_p\}  .    O  \mneq{}  p


By

---

Latex:
((Auto  THEN  D  -1  THEN  Unhide  THEN  Auto)  THEN  FLemma  `geo-between-sep`  [-1]\mcdot{}  THEN  Auto)

---

Home Index