let n be Element of NAT ; :: thesis: for x being Point of (TOP-REAL n) st not n is empty holds
x <> x + (1.REAL n)
let x be Point of (TOP-REAL n); :: thesis: ( not n is empty implies x <> x + (1.REAL n) )
A1: ( 0.REAL n = 0. (TOP-REAL n) & x = x + (0. (TOP-REAL n)) ) by EUCLID:27, EUCLID:66;
assume ( not n is empty & x = x + (1.REAL n) ) ; :: thesis: contradiction
hence contradiction by A1, Th2, REVROT_1:19; :: thesis: verum