---

Step * of Lemma geo-three-segment

No Annotations
∀e:EuclideanPlane. ∀[a,b,c,A,B,C:Point].  (ac ≅ AC) supposing (bc ≅ BC and ab ≅ AB and B(ABC) and B(abc))
BY
{ (Auto THEN gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A : Point
6. B : Point
7. C : Point
8. B(abc)
9. B(ABC)
10. ab ≅ AB
11. bc ≅ BC
12. a # b
⊢ ac ≅ AC

2
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. c : Point
5. A : Point
6. B : Point
7. C : Point
8. B(bbc)
9. B(ABC)
10. bb ≅ AB
11. bc ≅ BC
12. a ≡ b
⊢ bc ≅ AC

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,c,A,B,C:Point].    (ac  \mcong{}  AC)  supposing  (bc  \mcong{}  BC  and  ab  \mcong{}  AB  and  B(ABC)  and  B(abc))


By

---

Latex:
(Auto  THEN  gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index