let d, a, b, c be Element of REAL ; :: thesis: d ^2 <= (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 )
A1: 0 <= b ^2 by XREAL_1:65;
A2: 0 <= c ^2 by XREAL_1:65;
d ^2 <= (a ^2 ) + (d ^2 ) by XREAL_1:33, XREAL_1:65;
then 0 + (d ^2 ) <= ((a ^2 ) + (d ^2 )) + (c ^2 ) by A2, XREAL_1:9;
then 0 + (d ^2 ) <= (b ^2 ) + (((a ^2 ) + (d ^2 )) + (c ^2 )) by A1, XREAL_1:9;
hence d ^2 <= (((a ^2 ) + (b ^2 )) + (c ^2 )) + (d ^2 ) ; :: thesis: verum