---

Step * of Lemma angle-sum-functionality

∀e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k,a',b',c',x',y',z',i',j',k':Point.
  (a ≡ a'
  ⇒ b ≡ b'
  ⇒ c ≡ c'
  ⇒ x ≡ x'
  ⇒ y ≡ y'
  ⇒ z ≡ z'
  ⇒ i ≡ i'
  ⇒ j ≡ j'
  ⇒ k ≡ k'
  ⇒ (abc + xyz ≅a ijk ⇐⇒ a'b'c' + x'y'z' ≅a i'j'k'))
BY
{ ((Auto THEN (Unfold `angle-sum` -1 THEN ExRepD) THEN Unfold `angle-sum` 0 THEN GenRepD)
   THEN ((EliminatePoint (26) THEN Auto) THEN EliminatePoint (27) THEN Auto)
   THEN (EliminatePoint (28) THEN Auto)
   THEN (((EliminatePoint (25) THEN Auto) THEN EliminatePoint (24) THEN Auto) THEN EliminatePoint (23) THEN Auto)
   THEN ((EliminatePoint (22) THEN Auto) THEN EliminatePoint (21) THEN Auto)
   THEN EliminatePoint (20)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  (Unfold  `angle-sum`  -1  THEN  ExRepD)  THEN  Unfold  `angle-sum`  0  THEN  GenRepD)
  THEN  ((EliminatePoint  (26)  THEN  Auto)  THEN  EliminatePoint  (27)  THEN  Auto)
  THEN  (EliminatePoint  (28)  THEN  Auto)
  THEN  (((EliminatePoint  (25)  THEN  Auto)  THEN  EliminatePoint  (24)  THEN  Auto)
              THEN  EliminatePoint  (23)
              THEN  Auto)
  THEN  ((EliminatePoint  (22)  THEN  Auto)  THEN  EliminatePoint  (21)  THEN  Auto)
  THEN  EliminatePoint  (20)
  THEN  Auto)

---

Home Index