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:51;
[.0,s.[ c= [.0,1.]

proof

let x be object ; :: 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:18, TOPMETR:20;
A7: Q is open by Th11;
A8: f " is being_homeomorphism by A2, TOPS_2:56;
then A9: f " is one-to-one by TOPS_2:def 5;
rng (f ") = [#] I[01] by A8, TOPS_2:def 5;
then f " is onto by FUNCT_2:def 3;
then (f ") " = (f ") " by A9, TOPS_2:def 4;
then A10: ((f ") ") .: Q = (f ") " Q by A9, FUNCT_1:85;
A11: P1 = f .: Q by A1, A3, Th13;
f " is continuous by A2, TOPS_2:def 5;
hence P1 is open by A7, A4, A10, Lm1, A11, TOPS_2:43; :: thesis: verum