theorem Th8: :: EUCLID13:8

for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) st An <> Cn & An in Line (Bn,Cn) holds
Bn in Line (An,Cn)