---

Step * of Lemma pgeo-PLSepOr_wf

∀g:ProjectivePlaneStructure. ∀a:Point. ∀l:{l:Line| a ≠ l} . ∀m:Line.  (PLSepOr(a;l;m) ∈ a ≠ m ∨ m ≠ l)
BY
{ ((ProveWfLemma THEN D 1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlaneStructure.  \mforall{}a:Point.  \mforall{}l:\{l:Line|  a  \mneq{}  l\}  .  \mforall{}m:Line.
    (PLSepOr(a;l;m)  \mmember{}  a  \mneq{}  m  \mvee{}  m  \mneq{}  l)


By

---

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

---

Home Index