theorem Th5: :: EUCLID12:5

for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n)
for Ln being Element of line_of_REAL n st An <> Cn & Cn in LSeg (An,Bn) & An in Ln & Cn in Ln & Ln is being_line holds
Bn in Ln