---

Step * of Lemma pgeo-join-to-line-2

∀g:BasicProjectivePlane. ∀p,q:Point. ∀l:Line. ∀s:p ≠ q.  (p I l ⇒ q I l ⇒ l ≡ p ∨ q)
BY
{ ((((Auto THEN (Unfold `pgeo-leq` 0 THENA Auto)) THEN (D 0 THENA Auto))
    THEN (InstLemma `Unique` [⌜g⌝;⌜l⌝;⌜p ∨ q⌝;⌜p⌝;⌜q⌝]⋅ THENA Auto)
    )
   THEN D -1
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}g:BasicProjectivePlane.  \mforall{}p,q:Point.  \mforall{}l:Line.  \mforall{}s:p  \mneq{}  q.    (p  I  l  {}\mRightarrow{}  q  I  l  {}\mRightarrow{}  l  \mequiv{}  p  \mvee{}  q)


By

---

Latex:
((((Auto  THEN  (Unfold  `pgeo-leq`  0  THENA  Auto))  THEN  (D  0  THENA  Auto))
    THEN  (InstLemma  `Unique`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p  \mvee{}  q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
    )
  THEN  D  -1
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index