theorem Th1: :: TOPREAL9:3

for n being Nat
for x being Point of (TOP-REAL n) st not n is zero holds
x <> x + (1.REAL n)