theorem Th4: :: EUCLID12:4

for n being Nat
for An, Bn being Point of (TOP-REAL n)
for PAn, PBn being Element of REAL n st An = PAn & Bn = PBn holds
Line (An,Bn) = Line (PAn,PBn)