---

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


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
⊢ ab ≅ AB
BY
{ (InstHyp [⌜A⌝] (-5)⋅ THENA Auto) }

1
.....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

2
.....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
⊢ ca ≅ CA

3
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
14. ba ≅ BA
⊢ ab ≅ AB

---

Latex:

---

Latex:

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{}  ab  \mcong{}  AB


By

---

Latex:
(InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)

---

Home Index