let x, y be Complex; :: thesis: 2 * |.(x * y).| <= (|.x.| ^2 ) + (|.y.| ^2 )
set a = |.x.|;
set b = |.y.|;
(|.x.| - |.y.|) ^2 = ((|.x.| * |.x.|) - ((|.x.| * |.y.|) + (|.x.| * |.y.|))) + (|.y.| * |.y.|) ;
then ( |.x.| * |.y.| = |.(x * y).| & ((|.x.| * |.x.|) + (|.y.| * |.y.|)) - ((|.x.| * |.y.|) + (|.x.| * |.y.|)) >= 0 ) by COMPLEX1:151, XREAL_1:65;
hence 2 * |.(x * y).| <= (|.x.| ^2 ) + (|.y.| ^2 ) by XREAL_1:51; :: thesis: verum