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 )
assume x1 <> x2 ; :: thesis: |.(x1 - x2).| > 0
then 0 <> |.(x1 - x2).| by Th13;
hence |.(x1 - x2).| > 0 ; :: thesis: verum