---

Step * of Lemma LP-sep-or

∀g:ProjectivePlaneStructure. ∀l:Line. ∀p:Point.  (l ≠ p ⇒ (∀q:Point. (q ≠ l ∨ q ≠ p)))
BY
{ (Auto THEN UseWitness ⌜LPSepOr(l;p;q)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlaneStructure.  \mforall{}l:Line.  \mforall{}p:Point.    (l  \mneq{}  p  {}\mRightarrow{}  (\mforall{}q:Point.  (q  \mneq{}  l  \mvee{}  q  \mneq{}  p)))


By

---

Latex:
(Auto  THEN  UseWitness  \mkleeneopen{}LPSepOr(l;p;q)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index