theorem Th1: :: MESFUN17:1

for X, Y, Z being RealNormSpace
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.|| )