A1: now

let x, y be Complex; :: thesis: |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|)
A2: |.(x + y).| * |.(x + y).| = |.((x + y) * (x + y)).| by COMPLEX1:151
.= |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| ;
A3: ( |.(x * x).| = |.x.| * |.x.| & |.x.| ^2 = |.x.| * |.x.| & |.(y * y).| = |.y.| * |.y.| & |.y.| ^2 = |.y.| * |.y.| ) by COMPLEX1:151;
A4: ( |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| <= |.(((x * x) + (x * y)) + (x * y)).| + |.(y * y).| & |.(((x * x) + (x * y)) + (x * y)).| <= |.((x * x) + (x * y)).| + |.(x * y).| & |.((x * x) + (x * y)).| <= |.(x * x).| + |.(x * y).| ) by COMPLEX1:142;
then A5: ( |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| - |.(y * y).| <= |.(((x * x) + (x * y)) + (x * y)).| & |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).| <= |.((x * x) + (x * y)).| ) by XREAL_1:22;
then |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).| <= |.(x * x).| + |.(x * y).| by A4, XXREAL_0:2;
then |.(((x * x) + (x * y)) + (x * y)).| <= (|.(x * x).| + |.(x * y).|) + |.(x * y).| by XREAL_1:22;
then (|.(x + y).| * |.(x + y).|) - |.(y * y).| <= |.(x * x).| + (2 * |.(x * y).|) by A2, A5, XXREAL_0:2;
then A6: ((|.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).| <= 2 * |.(x * y).| by XREAL_1:22;
2 * |.(x * y).| <= (|.x.| ^2 ) + (|.y.| ^2 ) by Lm21;
then ((|.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).| <= (|.x.| ^2 ) + (|.y.| ^2 ) by A6, XXREAL_0:2;
then (|.(x + y).| * |.(x + y).|) - (|.y.| * |.y.|) <= ((|.x.| * |.x.|) + (|.y.| * |.y.|)) + (|.x.| * |.x.|) by A3, XREAL_1:22;
then |.(x + y).| * |.(x + y).| <= ((2 * (|.x.| * |.x.|)) + (|.y.| * |.y.|)) + (|.y.| * |.y.|) by XREAL_1:22;
hence |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) ; :: thesis: verum

end;

now

let x, y be Complex; :: 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 Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) & |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) ) by A1; :: thesis: verum