let X be RealUnitarySpace; :: thesis: for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||
let x, y be Point of X; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
A1: (x + y) .|. (x + y) >= 0 by Def2;
A2: ||.(x + y).|| ^2 >= 0 by XREAL_1:65;
A3: x .|. x >= 0 by Def2;
A4: y .|. y >= 0 by Def2;
sqrt (||.(x + y).|| ^2 ) = sqrt ((x + y) .|. (x + y)) by Th34, SQUARE_1:89;
then ||.(x + y).|| ^2 = (x + y) .|. (x + y) by A1, A2, SQUARE_1:96;
then ||.(x + y).|| ^2 = ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by Th21;
then A5: ||.(x + y).|| ^2 = (((sqrt (x .|. x)) ^2 ) + (2 * (x .|. y))) + (y .|. y) by A3, SQUARE_1:def 4;
A6: abs (x .|. y) <= ||.x.|| * ||.y.|| by Th24;
x .|. y <= abs (x .|. y) by ABSVALUE:11;
then x .|. y <= ||.x.|| * ||.y.|| by A6, XXREAL_0:2;
then 2 * (x .|. y) <= 2 * (||.x.|| * ||.y.||) by XREAL_1:66;
then (||.x.|| ^2 ) + (2 * (x .|. y)) <= (||.x.|| ^2 ) + ((2 * ||.x.||) * ||.y.||) by XREAL_1:9;
then ((||.x.|| ^2 ) + (2 * (x .|. y))) + (||.y.|| ^2 ) <= ((||.x.|| ^2 ) + ((2 * ||.x.||) * ||.y.||)) + (||.y.|| ^2 ) by XREAL_1:8;
then A7: ||.(x + y).|| ^2 <= (||.x.|| + ||.y.||) ^2 by A4, A5, SQUARE_1:def 4;
A8: ||.x.|| >= 0 by Th34;
||.y.|| >= 0 by Th34;
then ||.x.|| + ||.y.|| >= ||.x.|| + 0 by XREAL_1:9;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A7, A8, SQUARE_1:78; :: thesis: verum