theorem Th19: :: EUCLID13:22

for n being Nat
for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & r = 1 holds
|((Bn - Cn),(An - Bn))| = 0