---

Step * of Lemma hp-angle-sum-symm

∀e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k:Point.  (abc + xyz ≅ ijk ⇒ i # jk ⇒ xyz + abc ≅ ijk)
BY
{ (Auto THEN Unfold `hp-angle-sum` 0 THEN Unfold `hp-angle-sum` -2) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. ∃p,p',d',f':Point. (((abc ≅a ijp ∧ kjp ≅a xyz) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')
12. i # jk
⊢ ∃p,p',d',f':Point. (((xyz ≅a ijp ∧ kjp ≅a abc) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z,i,j,k:Point.    (abc  +  xyz  \mcong{}  ijk  {}\mRightarrow{}  i  \#  jk  {}\mRightarrow{}  xyz  +  abc  \mcong{}  ijk)


By

---

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

---

Home Index