---

Step * of Lemma geo-Aparallel-equiv

∀g:EuclideanParPlane. EquivRel(Line;l,m.l || m)
BY
{ (((Auto THEN (D 0 THEN Auto) THEN D 0 THEN Reduce 0 THEN Auto) THEN ((Unfold `geo-Aparallel` 0 THEN D 0) THENA Auto))
   THEN (Unfold `geo-intersect` -1 THEN GetLinePoints (2) THEN All Reduce⋅)
   THEN ExRepD
   THEN D 6
   THEN (((Unfold `geo-incident` 7 THEN Reduce 7⋅)
          THEN (InstLemma `not-lsep-iff-colinear` [⌜g⌝;⌜b⌝;⌜x⌝;⌜y⌝]⋅ THENA Auto)
          )
         THEN D -1
         )
   THEN ((Assert b # xy BY (Unfold `geo-lsep` 0 THEN Auto)) THEN D -2 THEN Auto)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanParPlane.  EquivRel(Line;l,m.l  ||  m)


By

---

Latex:
(((Auto  THEN  (D  0  THEN  Auto)  THEN  D  0  THEN  Reduce  0  THEN  Auto)
    THEN  ((Unfold  `geo-Aparallel`  0  THEN  D  0)  THENA  Auto)
    )
  THEN  (Unfold  `geo-intersect`  -1  THEN  GetLinePoints  (2)  THEN  All  Reduce\mcdot{})
  THEN  ExRepD
  THEN  D  6
  THEN  (((Unfold  `geo-incident`  7  THEN  Reduce  7\mcdot{})
                THEN  (InstLemma  `not-lsep-iff-colinear`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
                )
              THEN  D  -1
              )
  THEN  ((Assert  b  \#  xy  BY  (Unfold  `geo-lsep`  0  THEN  Auto))  THEN  D  -2  THEN  Auto)
  THEN  Auto)

---

Home Index