theorem Th18: :: EUCLID13:21

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