---

Step * 1 1 1 of Lemma Euclid-Prop17

.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. i : Point
6. j : Point
7. k : Point
8. a # bc
9. acb + abc ≅ ijk
10. a1 : Point
11. a2 : Point
12. a3 : Point
13. a1-a2-a3
14. d : Point
15. b-c-d
16. cd ≅ OX
17. abc < acd
18. acb + acd ≅ bcd
⊢ bcd ≅a a1a2a3
BY
{ (BLemma' `straight-angles-congruent`  THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  i  :  Point
6.  j  :  Point
7.  k  :  Point
8.  a  \#  bc
9.  acb  +  abc  \mcong{}  ijk
10.  a1  :  Point
11.  a2  :  Point
12.  a3  :  Point
13.  a1-a2-a3
14.  d  :  Point
15.  b-c-d
16.  cd  \mcong{}  OX
17.  abc  <  acd
18.  acb  +  acd  \mcong{}  bcd
\mvdash{}  bcd  \mcong{}\msuba{}  a1a2a3


By

---

Latex:
(BLemma'  `straight-angles-congruent`    THEN  Auto)

---

Home Index