---

Step * of Lemma pgeo-LPSepOr_wf

∀g:ProjectivePlaneStructure. ∀l:Line. ∀p:{p:Point| l ≠ p} . ∀q:Point.  (LPSepOr(l;p;q) ∈ q ≠ l ∨ q ≠ p)
BY
{ ((ProveWfLemma THEN D 1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlaneStructure.  \mforall{}l:Line.  \mforall{}p:\{p:Point|  l  \mneq{}  p\}  .  \mforall{}q:Point.
    (LPSepOr(l;p;q)  \mmember{}  q  \mneq{}  l  \mvee{}  q  \mneq{}  p)


By

---

Latex:
((ProveWfLemma  THEN  D  1)  THEN  Auto)

---

Home Index