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