theorem Th3: :: REAL_NS3:3

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