let a be Real; :: thesis: ( - 1 > a implies - a < a ^2 )
assume - 1 > a ; :: thesis: - a < a ^2
then - (- 1) < - a by XREAL_1:24;
then - a < (- a) ^2 by Th14;
hence - a < a ^2 ; :: thesis: verum