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