---

Step * of Lemma geo-seg-congruent_transitivity

No Annotations
∀e:BasicGeometry
  ∀[s1,s2,s3:geo-segment(e)].
    (geo-seg-congruent(e; s1; s3)) supposing (geo-seg-congruent(e; s1; s2) and geo-seg-congruent(e; s2; s3))
BY
{ (Auto THEN All (Unfold `geo-seg-congruent`) THEN FLemma `geo-congruent-transitivity` [-2;-1] THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry
    \mforall{}[s1,s2,s3:geo-segment(e)].
        (geo-seg-congruent(e;  s1;  s3))  supposing 
              (geo-seg-congruent(e;  s1;  s2)  and 
              geo-seg-congruent(e;  s2;  s3))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `geo-seg-congruent`)
  THEN  FLemma  `geo-congruent-transitivity`  [-2;-1]
  THEN  Auto)

---

Home Index