let n be Nat; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) holds |((An - Bn),(An - Cn))| = - |((An - Bn),(Cn - An))|
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: |((An - Bn),(An - Cn))| = - |((An - Bn),(Cn - An))|
reconsider rA = An, rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
|((rA - rB),(rA - rC))| = |((rA - rB),(- (rC - rA)))| by RVSUM_1:35
.= - |((rA - rB),(rC - rA))| by EUCLID_4:24 ;
hence |((An - Bn),(An - Cn))| = - |((An - Bn),(Cn - An))| ; :: thesis: verum