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