let n be Nat; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) holds |((Bn - An),(Cn - An))| = - |((Bn - An),(An - Cn))|
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: |((Bn - An),(Cn - An))| = - |((Bn - An),(An - Cn))|
|((Bn - An),(Cn - An))| = |((An - Bn),(An - Cn))| by Th15;
hence |((Bn - An),(Cn - An))| = - |((Bn - An),(An - Cn))| by Th14; :: thesis: verum