theorem Th3: :: JORDAN5A:3

for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st
( ( for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )