---

Step * of Lemma plsep-implies-ptriangle

∀g:ProjectivePlane. ∀p:Point. ∀l:Line. ∀q:Point. ∀s:q ≠ p.  (p ≠ l ⇒ q I l ⇒ (∃r:Point. (r I l ∧ r ≠ q ∨ p)))
BY
{ ((Auto THEN (Assert q ≠ p BY (InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜p⌝;⌜q⌝;⌜l⌝]⋅ THEN Auto)))
   THEN (InstLemma `point-implies-plsep-exists` [⌜g⌝;⌜q⌝]⋅ THEN Auto)
   THEN ExRepD) }

1
1. g : ProjectivePlane
2. p : Point
3. l : Line
4. q : Point
5. s : q ≠ p
6. p ≠ l
7. q I l
8. q ≠ p
9. l1 : Line
10. q ≠ l1
⊢ ∃r:Point. (r I l ∧ r ≠ q ∨ p)

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p:Point.  \mforall{}l:Line.  \mforall{}q:Point.  \mforall{}s:q  \mneq{}  p.
    (p  \mneq{}  l  {}\mRightarrow{}  q  I  l  {}\mRightarrow{}  (\mexists{}r:Point.  (r  I  l  \mwedge{}  r  \mneq{}  q  \mvee{}  p)))


By

---

Latex:
((Auto  THEN  (Assert  q  \mneq{}  p  BY  (InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)))
  THEN  (InstLemma  `point-implies-plsep-exists`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ExRepD)

---

Home Index