theorem Th2: :: REAL_NS3:2

for n being Nat
for x being Element of REAL (n + 1)
for w being Element of REAL st w = x . (n + 1) holds
|.w.| <= |.x.|