theorem :: EUCLID_4:38

for n being Nat
for x, y being Element of REAL n holds |.|(x,y)|.| <= |.x.| * |.y.|