Step
*
1
of Lemma
rabs_functionality
∀[x,y:ℝ].  rmax(x;-(x)) = rmax(y;-(y)) supposing x = y
BY
{ (Auto THEN RWO "-1" 0 THEN Auto) }
Latex:
Latex:
\mforall{}[x,y:\mBbbR{}].    rmax(x;-(x))  =  rmax(y;-(y))  supposing  x  =  y
By
Latex:
(Auto  THEN  RWO  "-1"  0  THEN  Auto)
Home
Index