---

Step * of Lemma pgeo-meet-to-point

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

---

Latex:

---

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


By

---

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

---

Home Index