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