let X, Y, Z be RealNormSpace; :: thesis: for u being Point of [:X,Y,Z:]
for x being Point of X
for y being Point of Y
for z being Point of Z st u = [x,y,z] holds
( ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| & ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )
let u be Point of [:X,Y,Z:]; :: thesis: for x being Point of X
for y being Point of Y
for z being Point of Z st u = [x,y,z] holds
( ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| & ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )
let x be Point of X; :: thesis: for y being Point of Y
for z being Point of Z st u = [x,y,z] holds
( ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| & ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )
let y be Point of Y; :: thesis: for z being Point of Z st u = [x,y,z] holds
( ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| & ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )
let z be Point of Z; :: thesis: ( u = [x,y,z] implies ( ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| & ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| ) )
assume u = [x,y,z] ; :: thesis: ( ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| & ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )
then A1: ||.u.|| = sqrt (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) by PRVECT_4:9;
(((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) + 0 <= (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) + ((2 * ||.x.||) * ||.y.||) by XREAL_1:7;
then (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) + 0 <= ((((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) + ((2 * ||.x.||) * ||.y.||)) + ((2 * ||.y.||) * ||.z.||) by XREAL_1:7;
then (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) + 0 <= (((((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) + ((2 * ||.x.||) * ||.y.||)) + ((2 * ||.y.||) * ||.z.||)) + ((2 * ||.x.||) * ||.z.||) by XREAL_1:7;
then sqrt (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) <= sqrt (((||.x.|| + ||.y.||) + ||.z.||) ^2) by SQUARE_1:26;
hence ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| by A1, SQUARE_1:22; :: thesis: ( ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )
( ||.x.|| ^2 <= (||.x.|| ^2) + (||.y.|| ^2) & (||.x.|| ^2) + (||.y.|| ^2) <= ((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2) ) by XREAL_1:31;
then ||.x.|| ^2 <= ((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2) by XXREAL_0:2;
then sqrt (||.x.|| ^2) <= sqrt (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) by SQUARE_1:26;
hence ||.x.|| <= ||.u.|| by A1, SQUARE_1:22; :: thesis: ( ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )
( ||.y.|| ^2 <= (||.x.|| ^2) + (||.y.|| ^2) & (||.x.|| ^2) + (||.y.|| ^2) <= ((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2) ) by XREAL_1:31;
then ||.y.|| ^2 <= ((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2) by XXREAL_0:2;
then sqrt (||.y.|| ^2) <= sqrt (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) by SQUARE_1:26;
hence ||.y.|| <= ||.u.|| by A1, SQUARE_1:22; :: thesis: ||.z.|| <= ||.u.||
sqrt (||.z.|| ^2) <= sqrt (((||.x.|| ^2) + (||.y.|| ^2)) + (||.z.|| ^2)) by SQUARE_1:26, XREAL_1:31;
hence ||.z.|| <= ||.u.|| by A1, SQUARE_1:22; :: thesis: verum