theorem NORMSP35: :: NDIFF_8:21

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )