---

Step * of Lemma geo-Aparallel_functionality

∀[e1:EuclideanPlane]. ∀[l,m,l2,m2:Line].  ({uiff(l || m;l2 || m2)}) supposing (m ≡ m2 and l ≡ l2)
BY
{ (Auto
   THEN (Assert l = l2 ∈ LINE BY
               (EqTypeCD THEN Auto))
   THEN (Assert m = m2 ∈ LINE BY
               (EqTypeCD THEN Auto))
   THEN D 0
   THEN RWO "-1 -2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e1:EuclideanPlane].  \mforall{}[l,m,l2,m2:Line].    (\{uiff(l  ||  m;l2  ||  m2)\})  supposing  (m  \mequiv{}  m2  and  l  \mequiv{}  l2)


By

---

Latex:
(Auto
  THEN  (Assert  l  =  l2  BY
                          (EqTypeCD  THEN  Auto))
  THEN  (Assert  m  =  m2  BY
                          (EqTypeCD  THEN  Auto))
  THEN  D  0
  THEN  RWO  "-1  -2"  0
  THEN  Auto)

---

Home Index