let n be Nat; for An, Bn, Cn being Point of (TOP-REAL n) st |((Bn - Cn),(Bn - Cn))| = - |((Cn - An),(Bn - Cn))| holds
|((Bn - Cn),(An - Bn))| = 0
let An, Bn, Cn be Point of (TOP-REAL n); ( |((Bn - Cn),(Bn - Cn))| = - |((Cn - An),(Bn - Cn))| implies |((Bn - Cn),(An - Bn))| = 0 )
assume A1:
|((Bn - Cn),(Bn - Cn))| = - |((Cn - An),(Bn - Cn))|
; |((Bn - Cn),(An - Bn))| = 0
reconsider rA = An, rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
|((rB - rC),(rB - rC))| + |((rB - rC),(rC - rA))| = 0
by A1;
then
|((rB - rC),((rB - rC) + (rC - rA)))| = 0
by EUCLID_4:28;
then
|((rB - rC),(((rB - rC) + rC) - rA))| = 0
by RVSUM_1:40;
then
|((Bn - Cn),(Bn - An))| = 0
by RVSUM_1:43;
then
- |((Bn - Cn),(An - Bn))| = 0
by Th14;
hence
|((Bn - Cn),(An - Bn))| = 0
; verum