theorem Th16: :: JORDAN20:16

for P being non empty Subset of (TOP-REAL 2)
for P1 being Subset of ((TOP-REAL 2) | P)
for f being Function of I[01],((TOP-REAL 2) | P)
for s being Real st s >= 0 & f is being_homeomorphism & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } holds
P1 is open