---

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


1. g : ProjectivePlane
2. p : Point
3. l : Line
4. p ≠ l
⊢ ∀q:Point. (q I l ⇒ p ≠ q)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜p⌝;⌜q⌝;⌜l⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  p  :  Point
3.  l  :  Line
4.  p  \mneq{}  l
\mvdash{}  \mforall{}q:Point.  (q  I  l  {}\mRightarrow{}  p  \mneq{}  q)


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index