---

Step * 1 1 of Lemma Euclid-Prop16-construction-lemma


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. d : Point
7. b=d=c
8. d # ca
9. y : Point
10. a-d-y
11. dy ≅ ad
12. b-d-c
13. y ≠ c
14. abd ≅a ycd
⊢ abc ≅a ycb
BY
{ (InstLemma `out-preserves-angle-cong_1` [⌜g⌝;⌜a⌝;⌜b⌝;⌜d⌝;⌜y⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜c⌝;⌜y⌝;⌜b⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  d  :  Point
7.  b=d=c
8.  d  \#  ca
9.  y  :  Point
10.  a-d-y
11.  dy  \mcong{}  ad
12.  b-d-c
13.  y  \mneq{}  c
14.  abd  \mcong{}\msuba{}  ycd
\mvdash{}  abc  \mcong{}\msuba{}  ycb


By

---

Latex:
(InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index