let a, b be real number ; :: thesis: 0 <= (a ^2 ) + (b ^2 )
( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:65;
hence 0 <= (a ^2 ) + (b ^2 ) ; :: thesis: verum