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 A1: ( 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 ) } ) ; :: thesis: P1 is open
[.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 A2: x in [.0 ,s.[ ; :: thesis: x in [.0 ,1.]
then reconsider sx = x as Real ;
( 0 <= sx & sx < s ) by A2, XXREAL_1:3;
then ( 0 <= sx & sx < 1 ) by A1, XXREAL_0:2;
hence x in [.0 ,1.] by XXREAL_1:1; :: thesis: verum

end;

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