theorem Th7: :: EUCLID13:7

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