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) )
assume that
A1: not n is empty and
A2: x = x + (1.REAL n) ; :: thesis: contradiction
X: 0.REAL n = 0. (TOP-REAL n) by EUCLID:70;
x = x + (0. (TOP-REAL n)) by EUCLID:31;
hence contradiction by A1, A2, Th2, X, REVROT_1:19; :: thesis: verum