let r be Real; :: thesis: [/r\] = [\r/] + (sgn (frac r))

per cases ( r is integer or not r is integer ) ;

suppose r is integer ; :: thesis: [/r\] = [\r/] + (sgn (frac r))

then reconsider r = r as integer Real ;
[/r\] = [\r/] + (sgn (frac r)) ;
hence [/r\] = [\r/] + (sgn (frac r)) ; :: thesis: verum

end;

suppose not r is integer ; :: thesis: [/r\] = [\r/] + (sgn (frac r))

then reconsider r = r as non integer Real ;
reconsider f = frac r as positive Real ;
[/r\] = [\r/] + 1 by INT_1:34, INT_1:41
.= [\r/] + (sgn f) by ABSVALUE:def 2 ;
hence [/r\] = [\r/] + (sgn (frac r)) ; :: thesis: verum

end;

end;