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