theorem Th1: :: REAL_NS3:1

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