let n be Nat; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) holds |((An - Bn),(An - Cn))| = |((Bn - An),(Cn - An))|
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: |((An - Bn),(An - Cn))| = |((Bn - An),(Cn - An))|
A1: |((An - Bn),(An - Cn))| = |((- (An - Bn)),(- (An - Cn)))| by EUCLID_2:23;
( - (An - Bn) = Bn - An & - (Cn - An) = An - Cn ) by RVSUM_1:35;
hence |((An - Bn),(An - Cn))| = |((Bn - An),(Cn - An))| by A1; :: thesis: verum