let a, b be real number ; :: thesis: ( a < 0 & 0 < b implies a " < b " )
assume ( a < 0 & b > 0 ) ; :: thesis: a " < b "
then ( a " < 0 & b " > 0 ) ;
hence a " < b " ; :: thesis: verum