let n be Nat; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & |((Bn - An),(Bn - Cn))| = 0 holds
An <> Cn
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: ( Bn <> Cn & |((Bn - An),(Bn - Cn))| = 0 implies An <> Cn )
assume that
A1: Bn <> Cn and
A2: |((Bn - An),(Bn - Cn))| = 0 ; :: thesis: An <> Cn
assume A3: An = Cn ; :: thesis: contradiction
reconsider rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
rB - rC = 0* n by A2, A3, EUCLID_4:17;
hence contradiction by A1, EUCLIDLP:9; :: thesis: verum