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: sqrt (||.(x + y).|| ^2) = sqrt ((x + y) .|. (x + y)) by Th28, SQUARE_1:22;
( (x + y) .|. (x + y) >= 0 & ||.(x + y).|| ^2 >= 0 ) by Def2, XREAL_1:63;
then ||.(x + y).|| ^2 = (x + y) .|. (x + y) by A1, SQUARE_1:28;
then A2: ||.(x + y).|| ^2 = ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by Th16;
x .|. x >= 0 by Def2;
then A3: ||.(x + y).|| ^2 = (((sqrt (x .|. x)) ^2) + (2 * (x .|. y))) + (y .|. y) by A2, SQUARE_1:def 2;
A4: ( ||.x.|| >= 0 & ||.y.|| >= 0 ) by Th28;
( |.(x .|. y).| <= ||.x.|| * ||.y.|| & x .|. y <= |.(x .|. y).| ) by Th19, ABSVALUE:4;
then x .|. y <= ||.x.|| * ||.y.|| by XXREAL_0:2;
then 2 * (x .|. y) <= 2 * (||.x.|| * ||.y.||) by XREAL_1:64;
then (||.x.|| ^2) + (2 * (x .|. y)) <= (||.x.|| ^2) + ((2 * ||.x.||) * ||.y.||) by XREAL_1:7;
then A5: ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) <= ((||.x.|| ^2) + ((2 * ||.x.||) * ||.y.||)) + (||.y.|| ^2) by XREAL_1:6;
y .|. y >= 0 by Def2;
then ||.(x + y).|| ^2 <= (||.x.|| + ||.y.||) ^2 by A3, A5, SQUARE_1:def 2;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A4, SQUARE_1:16; :: thesis: verum