---

Step * 1 1 1 of Lemma geo-inner-three-segment

.....antecedent..... 
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))
6. A : Point
7. B : Point
8. C : Point
9. ∀[D:Point]. (ba ≅ BD) supposing (ca ≅ CD and aa ≅ AD and bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
10. B(abc)
11. B(ABC)
12. ac ≅ AC
13. bc ≅ BC
⊢ aa ≅ AA
BY
{ (UseEuAxioms THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  \mforall{}[d,A,B,C,D:Point].
          (bd  \mcong{}  BD)  supposing  (cd  \mcong{}  CD  and  ad  \mcong{}  AD  and  bc  \mcong{}  BC  and  ac  \mcong{}  AC  and  B(ABC)  and  B(abc))
6.  A  :  Point
7.  B  :  Point
8.  C  :  Point
9.  \mforall{}[D:Point]
          (ba  \mcong{}  BD)  supposing  (ca  \mcong{}  CD  and  aa  \mcong{}  AD  and  bc  \mcong{}  BC  and  ac  \mcong{}  AC  and  B(ABC)  and  B(abc))
10.  B(abc)
11.  B(ABC)
12.  ac  \mcong{}  AC
13.  bc  \mcong{}  BC
\mvdash{}  aa  \mcong{}  AA


By

---

Latex:
(UseEuAxioms  THEN  BackThruSomeHyp)

---

Home Index