let a be real number ; :: thesis: ( - 1 > a implies - a < a ^2 )
assume - 1 > a ; :: thesis: - a < a ^2
then - (- 1) < - a by XREAL_1:26;
then - a < (- a) ^2 by Th76;
hence - a < a ^2 ; :: thesis: verum