A1:
now for x, y being Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y)end;
now for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y)let x,
y be
Real;
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;
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; verum