---

Step * 1 of Lemma eu-seg-congruent-equiv-proper


1. e : EuclideanPlane@i'
2. Sym(ProperSegment;s,t.s ≡ t)
3. a : ProperSegment@i
4. b : ProperSegment@i
5. c : ProperSegment@i
6. a ≡ b@i
7. b ≡ c@i
⊢ a ≡ c
BY
{ (FLemma  `eu-seg-congruent_transitivity` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  Sym(ProperSegment;s,t.s  \mequiv{}  t)
3.  a  :  ProperSegment@i
4.  b  :  ProperSegment@i
5.  c  :  ProperSegment@i
6.  a  \mequiv{}  b@i
7.  b  \mequiv{}  c@i
\mvdash{}  a  \mequiv{}  c


By

---

Latex:
(FLemma    `eu-seg-congruent\_transitivity`  [-1;-2]  THEN  Auto)

---

Home Index