---

Step * of Lemma geo-add-length_functionality_wrt_cong

∀e:BasicGeometry. ∀x,y,x',y':Length.  ((x = x' ∈ Length) ⇒ (y = y' ∈ Length) ⇒ (x + y = x' + y' ∈ Length))
BY
{ (Auto THEN UseWitness ⌜Ax⌝⋅) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}x,y,x',y':Length.    ((x  =  x')  {}\mRightarrow{}  (y  =  y')  {}\mRightarrow{}  (x  +  y  =  x'  +  y'))


By

---

Latex:
(Auto  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{})

---

Home Index