let a, x be real number ; :: thesis: ( a <= 0 & x < a implies x ^2 > a ^2 )
assume A1: ( a <= 0 & x < a ) ; :: thesis: x ^2 > a ^2
then - (- a) <= 0 ;
then A2: - a >= 0 ;
- x > - a by A1, XREAL_1:26;
then (- x) ^2 > (- a) ^2 by A2, Th78;
hence x ^2 > a ^2 ; :: thesis: verum