let a, b be Real; :: thesis: ( a < 0 & 0 < b implies a " < b " )
assume that
A1: a < 0 and
A2: b > 0 ; :: thesis: a " < b "
a " < 0 by A1;
hence a " < b " by A2; :: thesis: verum