let a, b be Real; :: thesis: 0 <= (a ^2) + (b ^2)
( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63;
then 0 + 0 <= (a ^2) + (b ^2) ;
hence 0 <= (a ^2) + (b ^2) ; :: thesis: verum