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