---

Step * of Lemma pgeo-meet-implies-plsep

∀g:BasicProjectivePlane. ∀a,b,c:Line. ∀s:a ≠ b.  (a ∧ b ≠ c ⇒ (∀l:Point. ((l I a ∧ l I b) ⇒ l ≠ c)))
BY
{ ProveDualLemma `pgeo-join-implies-plsep` }

---

Latex:

---

Latex:
\mforall{}g:BasicProjectivePlane.  \mforall{}a,b,c:Line.  \mforall{}s:a  \mneq{}  b.
    (a  \mwedge{}  b  \mneq{}  c  {}\mRightarrow{}  (\mforall{}l:Point.  ((l  I  a  \mwedge{}  l  I  b)  {}\mRightarrow{}  l  \mneq{}  c)))


By

---

Latex:
ProveDualLemma  `pgeo-join-implies-plsep`

---

Home Index