theorem Th14: :: REAL_NS3:13

for n being non empty Nat
for x being Element of REAL n holds
( (sum_norm n) . x <= n * ((max_norm n) . x) & (max_norm n) . x <= |.x.| & |.x.| <= (sum_norm n) . x )