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