let P be non empty Subset of (TOP-REAL 2); :: thesis: 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
let P1 be Subset of ((TOP-REAL 2) | P); :: thesis: 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
let f be Function of I[01] ,((TOP-REAL 2) | P); :: thesis: 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
let s be Real; :: thesis: ( 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 ) } implies P1 is open )
A1: [#] I[01] <> {} ;
assume A2: ( 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 ) } ) ; :: thesis: P1 is open
].s,1.] c= [.0 ,1.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].s,1.] or x in [.0 ,1.] )
assume A3: x in ].s,1.] ; :: thesis: x in [.0 ,1.]
then reconsider sx = x as Real ;
( 0 < sx & sx <= 1 ) by A2, A3, XXREAL_1:2;
hence x in [.0 ,1.] by XXREAL_1:1; :: thesis: verum

end;

then reconsider Q = ].s,1.] as Subset of I[01] by TOPMETR:25, TOPMETR:27;
A4: Q is open by Th12;
A5: P1 = f .: Q by A2, Th14;
( f is one-to-one & rng f = [#] ((TOP-REAL 2) | P) ) by A2, TOPS_2:def 5;
then A6: (f " ) " = f by TOPS_2:64;
A7: f " is being_homeomorphism by A2, TOPS_2:70;
then A8: rng (f " ) = [#] I[01] by TOPS_2:def 5;
A9: f " is one-to-one by A7, TOPS_2:def 5;
then (f " ) " = (f " ) " by A8, TOPS_2:def 4;
then A10: ((f " ) " ) .: Q = (f " ) " Q by A9, FUNCT_1:155;
f " is continuous by A2, TOPS_2:def 5;
hence P1 is open by A1, A4, A5, A6, A10, TOPS_2:55; :: thesis: verum