---

Step * of Lemma geo-cong-angle_functionality

∀e:EuclideanPlane. ∀a1,a2,b1,b2,c1,c2,d1,d2,f1,f2,g1,g2:Point.
  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ d1 ≡ d2 ⇒ f1 ≡ f2 ⇒ g1 ≡ g2 ⇒ (a1b1c1 ≅a d1f1g1 ⇐⇒ a2b2c2 ≅a d2f2g2))
BY
{ (Auto THEN ParallelLast THEN (∀h:hyp. gEliminatePoint h  THENA Auto) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a1,a2,b1,b2,c1,c2,d1,d2,f1,f2,g1,g2:Point.
    (a1  \mequiv{}  a2
    {}\mRightarrow{}  b1  \mequiv{}  b2
    {}\mRightarrow{}  c1  \mequiv{}  c2
    {}\mRightarrow{}  d1  \mequiv{}  d2
    {}\mRightarrow{}  f1  \mequiv{}  f2
    {}\mRightarrow{}  g1  \mequiv{}  g2
    {}\mRightarrow{}  (a1b1c1  \mcong{}\msuba{}  d1f1g1  \mLeftarrow{}{}\mRightarrow{}  a2b2c2  \mcong{}\msuba{}  d2f2g2))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  (\mforall{}h:hyp.  gEliminatePoint  h    THENA  Auto)  THEN  Auto)

---

Home Index