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