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 )
assume that
A1: s >= 0 and
A2: f is being_homeomorphism and
A3: 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
( f is one-to-one & rng f = [#] ((TOP-REAL 2) | P) ) by A2, TOPS_2:def 5;
then A4: (f ") " = f by TOPS_2:51;
].s,1.] c= [.0,1.]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].s,1.] or x in [.0,1.] )
assume A5: x in ].s,1.] ; :: thesis: x in [.0,1.]
then reconsider sx = x as Real ;
( 0 < sx & sx <= 1 ) by A1, A5, 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:18, TOPMETR:20;
A6: ( [#] I[01] <> {} & Q is open ) by Th12;
A7: f " is being_homeomorphism by A2, TOPS_2:56;
then A8: f " is one-to-one by TOPS_2:def 5;
rng (f ") = [#] I[01] by A7, TOPS_2:def 5;
then f " is onto by FUNCT_2:def 3;
then (f ") " = (f ") " by A8, TOPS_2:def 4;
then A9: ((f ") ") .: Q = (f ") " Q by A8, FUNCT_1:85;
( P1 = f .: Q & f " is continuous ) by A1, A2, A3, Th14, TOPS_2:def 5;
hence P1 is open by A6, A4, A9, TOPS_2:43; :: thesis: verum