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 XREAL_1:153;
hence - a <= a ^2 ; :: thesis: verum