let r be heavy Real; :: thesis: ( sgn r = sgn [\r/] & sgn r = sgn [/r\] )

per cases ( r is negative or r is positive ) ;

suppose r is negative ; :: thesis: ( sgn r = sgn [\r/] & sgn r = sgn [/r\] )

then reconsider r = r as negative Real ;
( sgn [\r/] = - 1 & sgn [/r\] = - 1 & sgn r = - 1 ) by ABSVALUE:def 2;
hence ( sgn r = sgn [\r/] & sgn r = sgn [/r\] ) ; :: thesis: verum

end;

suppose r is positive ; :: thesis: ( sgn r = sgn [\r/] & sgn r = sgn [/r\] )

then reconsider r = r as positive Real ;
( sgn [\r/] = 1 & sgn [/r\] = 1 & sgn r = 1 ) by ABSVALUE:def 2;
hence ( sgn r = sgn [\r/] & sgn r = sgn [/r\] ) ; :: thesis: verum

end;

end;