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