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