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 <= 1 & f is being_homeomorphism & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } holds
P1 is open