---

Step * 2 of Lemma Euclid-prop13


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a # cd
8. a ≠ b
⊢ abc + abd ≅ cbd
BY
{ (Unfold `hp-angle-sum` 0 THEN InstConcl [⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  c-b-d
7.  a  \#  cd
8.  a  \mneq{}  b
\mvdash{}  abc  +  abd  \mcong{}  cbd


By

---

Latex:
(Unfold  `hp-angle-sum`  0  THEN  InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index