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