theorem Th10: :: EUCLID13:11

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