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