---

Step * of Lemma hp-angle-sum-sep

∀e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k:Point.  (abc + xyz ≅ ijk ⇒ {i ≠ j ∧ j ≠ k})
BY
{ ((Auto THEN Unfold `hp-angle-sum` -1 THEN ExRepD) THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  Unfold  `hp-angle-sum`  -1  THEN  ExRepD)  THEN  EAuto  1)

---

Home Index