let a be real number ; :: thesis: ( a < - 1 implies - 1 < a " )
( a < - 1 implies (- 1) " < a " ) by Lm35;
hence ( a < - 1 implies - 1 < a " ) ; :: thesis: verum