theorem Th11: :: EUCLID13:12

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