theorem Th17: :: EUCLID13:18

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