---

Step * of Lemma rabs*_functionality

∀[x,y:ℝ*].  (x = y ⇒ |x| = |y|)
BY
{ (Intros THEN Unfold `rabs*` 0 THEN BLemma `rfun*_functionality` THEN Auto THEN Reduce 0 THEN RWO  "-1" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}*].    (x  =  y  {}\mRightarrow{}  |x|  =  |y|)


By

---

Latex:
(Intros
  THEN  Unfold  `rabs*`  0
  THEN  BLemma  `rfun*\_functionality`
  THEN  Auto
  THEN  Reduce  0
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index