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 by A2, EUCLID_4:16;
then x1 - x2 = 0* n by EUCLID_4:17;
then x1 = x2 + (0* n) by Th6
.= x2 by EUCLID_4:1 ;
hence contradiction by A1; :: thesis: verum

end;

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