let a, b be Real; :: thesis: ( sgn a > sgn b implies a > b )
assume A1: sgn a > sgn b ; :: thesis: a > b
( a > 0 or a = 0 or a < 0 ) ;
then A2: ( sgn a = 1 or sgn a = 0 or sgn a = - 1 ) by ABSVALUE:def 2;
( b > 0 or b = 0 or b < 0 ) ;
hence a > b by A1, A2, ABSVALUE:def 2; :: thesis: verum