let n be Nat; 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); |((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; verum