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