---

Step * of Lemma pgeo-peq_transitivity

∀g:ProjectivePlane. ∀a,b,c:Point.  (a ≡ b ⇒ b ≡ c ⇒ a ≡ c)
BY
{ (((((Auto THEN D 0) THENA Auto) THEN Unfold `pgeo-psep` -1) THEN ExRepD)
   THEN ((InstLemma`pgeo-peq-preserves-incidence` [⌜g⌝;⌜a⌝;⌜b⌝;⌜l⌝]⋅ THENA EAuto 1)
         THEN (InstLemma`pgeo-peq-preserves-incidence` [⌜g⌝;⌜b⌝;⌜c⌝;⌜l⌝]⋅ THENA EAuto 1)
         )
   THEN D 11
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  b  \mequiv{}  c  {}\mRightarrow{}  a  \mequiv{}  c)


By

---

Latex:
(((((Auto  THEN  D  0)  THENA  Auto)  THEN  Unfold  `pgeo-psep`  -1)  THEN  ExRepD)
  THEN  ((InstLemma`pgeo-peq-preserves-incidence`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
              THEN  (InstLemma`pgeo-peq-preserves-incidence`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
              )
  THEN  D  11
  THEN  Auto)

---

Home Index