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 <= 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
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 <= 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
let f be Function of I[01] ,((TOP-REAL 2) | P); :: thesis: 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
let s be Real; :: thesis: ( 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 ) } implies P1 is open )
assume that
A1: s <= 1 and
A2: f is being_homeomorphism and
A3: P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & 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:64;
[.0 ,s.[ c= [.0 ,1.]

proof

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

end;

then reconsider Q = [.0 ,s.[ as Subset of I[01] by TOPMETR:25, TOPMETR:27;
A7: Q is open by Th11;
A8: f " is being_homeomorphism by A2, TOPS_2:70;
then A9: f " is one-to-one by TOPS_2:def 5;
rng (f " ) = [#] I[01] by A8, TOPS_2:def 5;
then (f " ) " = (f " ) " by A9, TOPS_2:def 4;
then A10: ((f " ) " ) .: Q = (f " ) " Q by A9, FUNCT_1:155;
( P1 = f .: Q & f " is continuous ) by A1, A2, A3, Th13, TOPS_2:def 5;
hence P1 is open by A7, A4, A10, Lm1, TOPS_2:55; :: thesis: verum