let a be Real; :: thesis: ( 1 <= a implies a " <= 1 )
( 1 <= a implies a " <= 1 " ) by Lm32;
hence ( 1 <= a implies a " <= 1 ) ; :: thesis: verum