theorem Th22: :: REAL_NS3:21

for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for x being Element of X st dim X <> 0 holds
( (sum_norm (X,b)) . x <= (dim X) * ((max_norm (X,b)) . x) & (max_norm (X,b)) . x <= (euclid_norm (X,b)) . x & (euclid_norm (X,b)) . x <= (sum_norm (X,b)) . x )