let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
let x1, x2 be Element of REAL n; :: thesis: ( x1 <> x2 implies |.(x1 - x2).| <> 0 )

now :: thesis: ( x1 <> x2 implies |.(x1 - x2).| <> 0 )

assume that
A1: x1 <> x2 and
A2: not |.(x1 - x2).| <> 0 ; :: thesis: contradiction
|((x1 - x2),(x1 - x2))| = 0 ^2 by A2, EUCLID_2:4;
then x1 - x2 = 0* n by Th17;
then x1 = x1 - (x1 + (- x2)) by RVSUM_1:32
.= (x1 - x1) - (- x2) by RVSUM_1:39
.= (0* n) - (- x2) by RVSUM_1:37
.= x2 by RVSUM_1:33 ;
hence contradiction by A1; :: thesis: verum

end;

hence ( x1 <> x2 implies |.(x1 - x2).| <> 0 ) ; :: thesis: verum