let n be Nat; 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); ( Bn <> Cn & |((Bn - An),(Bn - Cn))| = 0 implies An <> Cn )
assume that
A1:
Bn <> Cn
and
A2:
|((Bn - An),(Bn - Cn))| = 0
; An <> Cn
assume A3:
An = Cn
; 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; verum