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 = x + (0.REAL n) by EUCLID:31;
hence contradiction by A1, A2, Th2, REVROT_1:19; :: thesis: verum