---

Step * of Lemma pgeo-plsep-iff-all-psep

∀g:ProjectivePlane. ∀p:Point. ∀l:Line.  (p ≠ l ⇐⇒ ∀q:Point. (q I l ⇒ p ≠ q))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. g : ProjectivePlane
2. p : Point
3. l : Line
4. p ≠ l
⊢ ∀q:Point. (q I l ⇒ p ≠ q)

2
1. g : ProjectivePlane
2. p : Point
3. l : Line
4. ∀q:Point. (q I l ⇒ p ≠ q)
⊢ p ≠ l

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p:Point.  \mforall{}l:Line.    (p  \mneq{}  l  \mLeftarrow{}{}\mRightarrow{}  \mforall{}q:Point.  (q  I  l  {}\mRightarrow{}  p  \mneq{}  q))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index