let a, x be Real; :: thesis: ( a <= 0 & x < a implies x ^2 > a ^2 )
assume that
A1: a <= 0 and
A2: x < a ; :: thesis: x ^2 > a ^2
- x > - a by A2, XREAL_1:24;
then (- x) ^2 > (- a) ^2 by A1, Th16;
hence x ^2 > a ^2 ; :: thesis: verum