theorem Th15: :: EUCLID13:16

for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) holds |((Bn - An),(Cn - An))| = |((An - Bn),(An - Cn))|