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