let n be Nat; :: thesis: for x being Point of (TOP-REAL n) st not n is zero holds
x <> x + (1.REAL n)
let x be Point of (TOP-REAL n); :: thesis: ( not n is zero implies x <> x + (1.REAL n) )
A1: ( 0.REAL n = 0. (TOP-REAL n) & x = x + (0. (TOP-REAL n)) ) by EUCLID:66, RLVECT_1:4;
assume that
A2: not n is zero and
A3: x = x + (1.REAL n) ; :: thesis: contradiction
0.REAL n <> 1.REAL n by A2, REVROT_1:19;
hence contradiction by A1, A3, RLVECT_1:8; :: thesis: verum