let a be Real; :: thesis: sgn (frac a) = sgn (frac (- a))

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

suppose a is integer ; :: thesis: sgn (frac a) = sgn (frac (- a))

hence sgn (frac a) = sgn (frac (- a)) ; :: thesis: verum

end;

suppose not a is integer ; :: thesis: sgn (frac a) = sgn (frac (- a))

then ( sgn (frac a) = 1 & sgn (frac (- a)) = 1 ) by COMPLEX3:1;
hence sgn (frac a) = sgn (frac (- a)) ; :: thesis: verum

end;

end;