---

Step * of Lemma hp-angle-sum-subst4

∀g:EuclideanPlane. ∀a,b,c,d,e,f,x,y,z,i,j,k:Point.
  (abc + def ≅ xyz ⇒ xyz ≅a ijk ⇒ x-y-z ⇒ a # bc ⇒ d # ef ⇒ abc + def ≅ ijk)
BY
{ (((Auto THEN Unfold `hp-angle-sum` 0) THEN Unfold `hp-angle-sum` -5) THEN ExRepD) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. a # bc
27. d # ef
⊢ ∃p,p',d',f':Point. (((abc ≅a ijp ∧ kjp ≅a def) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f,x,y,z,i,j,k:Point.
    (abc  +  def  \mcong{}  xyz  {}\mRightarrow{}  xyz  \mcong{}\msuba{}  ijk  {}\mRightarrow{}  x-y-z  {}\mRightarrow{}  a  \#  bc  {}\mRightarrow{}  d  \#  ef  {}\mRightarrow{}  abc  +  def  \mcong{}  ijk)


By

---

Latex:
(((Auto  THEN  Unfold  `hp-angle-sum`  0)  THEN  Unfold  `hp-angle-sum`  -5)  THEN  ExRepD)

---

Home Index