A1: now

let x, y be Real; :: thesis: (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y)
0 <= (x - y) ^2 by XREAL_1:65;
then 0 + ((x + y) * (x + y)) <= ((((2 * x) * x) + ((2 * y) * y)) - ((x + y) * (x + y))) + ((x + y) * (x + y)) by XREAL_1:9;
hence (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ; :: thesis: verum

end;

now

let x, y be Real; :: thesis: x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y)
(x - y) + y = x ;
hence x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) by A1; :: thesis: verum

end;

hence ( ( for x, y being Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) & ( for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) ) by A1; :: thesis: verum