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