---

Step * of Lemma pgeo-lsep-implies-plsep

∀g:ProjectivePlane. ∀p:Point. ∀l,m:Line. ∀s:l ≠ m.  (p I l ⇒ p ≠ l ∧ m ⇒ p ≠ m)
BY
{ Auto }

1
1. g : ProjectivePlane
2. p : Point
3. l : Line
4. m : Line
5. s : l ≠ m
6. p I l
7. p ≠ l ∧ m
⊢ p ≠ m

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p:Point.  \mforall{}l,m:Line.  \mforall{}s:l  \mneq{}  m.    (p  I  l  {}\mRightarrow{}  p  \mneq{}  l  \mwedge{}  m  {}\mRightarrow{}  p  \mneq{}  m)


By

---

Latex:
Auto

---

Home Index