---

Step * of Lemma pgeo-psep-or

∀g:ProjectivePlane. ∀p,q,r:Point.  (p ≠ q ⇒ {p ≠ r ∨ r ≠ q})
BY
{ (((((Auto THEN Duplicate 5) THEN D -1) THEN ExRepD) THEN InstLemma `LP-sep-or2` [⌜g⌝;⌜l⌝;⌜q⌝;⌜r⌝]⋅ THEN Auto)
   THEN (D -1 THEN Auto)
   THEN ((InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜r⌝;⌜p⌝;⌜l⌝]⋅ THEN Auto) THEN OrLeft)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p,q,r:Point.    (p  \mneq{}  q  {}\mRightarrow{}  \{p  \mneq{}  r  \mvee{}  r  \mneq{}  q\})


By

---

Latex:
(((((Auto  THEN  Duplicate  5)  THEN  D  -1)  THEN  ExRepD)
    THEN  InstLemma  `LP-sep-or2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  (D  -1  THEN  Auto)
  THEN  ((InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  OrLeft)
  THEN  Auto)

---

Home Index