theorem :: CSSPACE2:5

for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) & |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) ) by Lm21;