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 ") " < (b ") " by A1, A2, Th124;
hence a < b ; :: thesis: verum