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