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