let a, b be Real; :: thesis: ( a >= 0 & b >= 0 & a ^2 >= b ^2 implies a >= b )
assume that
A1: a >= 0 and
A2: b >= 0 and
A3: a ^2 >= b ^2 ; :: thesis: a >= b
sqrt (a ^2) >= sqrt (b ^2) by A2, A3, SQUARE_1:26;
then a >= sqrt (b ^2) by A1, SQUARE_1:22;
hence a >= b by A1, SQUARE_1:22; :: thesis: verum