---

Step * of Lemma geo-inner-three-segment

No Annotations
∀e:EuclideanPlane. ∀[a,b,c,A,B,C:Point].  (ab ≅ AB) supposing (bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
BY
{ (InstLemma `geo-inner-five-segment` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. e : EuclideanPlane
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. ∀[d,A,B,C,D:Point].  (bd ≅ BD) supposing (cd ≅ CD and ad ≅ AD and bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
⊢ ∀[A,B,C:Point].  (ab ≅ AB) supposing (bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `geo-inner-five-segment`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index