theorem Th15: :: LOPBAN_7:15

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