theorem :: RSSPACE2:4

( ( 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 Lm2;