let P be Subset of I[01] ; :: thesis: for s being Real st P = [.0 ,s.[ holds
P is open
let s be Real; :: thesis: ( P = [.0 ,s.[ implies P is open )
assume A1: P = [.0 ,s.[ ; :: thesis: P is open
A2: [#] I[01] = [.0 ,1.] by TOPMETR:25, TOPMETR:27;

per cases ( s in [.0 ,1.] or not s in [.0 ,1.] ) ;

suppose A3: s in [.0 ,1.] ; :: thesis: P is open

then A4: ( 0 <= s & s <= 1 ) by XXREAL_1:1;
reconsider Q = ].(- 1),s.[ as Subset of R^1 by TOPMETR:24;
A5: Q is open by JORDAN6:46;
reconsider T = [.0 ,1.] as Subset of R^1 by TOPMETR:24;
A6: [.0 ,s.[ c= [.0 ,s.] by XXREAL_1:24;
0 in [.0 ,1.] by XXREAL_1:1;
then [.0 ,s.] c= [.0 ,1.] by A3, XXREAL_2:def 12;
then [.0 ,s.[ c= [.0 ,1.] by A6, XBOOLE_1:1;
then P c= [#] (R^1 | T) by A1, PRE_TOPC:def 10;
then reconsider P2 = P as Subset of (R^1 | T) ;
A7: ].(- 1),s.[ /\ [.0 ,1.] c= [.0 ,s.[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].(- 1),s.[ /\ [.0 ,1.] or x in [.0 ,s.[ )
assume A8: x in ].(- 1),s.[ /\ [.0 ,1.] ; :: thesis: x in [.0 ,s.[
then A9: ( x in ].(- 1),s.[ & x in [.0 ,1.] ) by XBOOLE_0:def 4;
reconsider sx = x as Real by A8;
A10: ( - 1 < sx & sx < s ) by A9, XXREAL_1:4;
( 0 <= sx & sx <= 1 ) by A9, XXREAL_1:1;
hence x in [.0 ,s.[ by A10, XXREAL_1:3; :: thesis: verum

end;

[.0 ,s.[ c= ].(- 1),s.[ /\ [.0 ,1.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.0 ,s.[ or x in ].(- 1),s.[ /\ [.0 ,1.] )
assume A11: x in [.0 ,s.[ ; :: thesis: x in ].(- 1),s.[ /\ [.0 ,1.]
then reconsider sx = x as Real ;
A12: ( 0 <= sx & sx < s ) by A11, XXREAL_1:3;
then A13: sx <= 1 by A4, XXREAL_0:2;
- 1 < sx by A12, XXREAL_0:2;
then ( x in ].(- 1),s.[ & x in [.0 ,1.] ) by A12, A13, XXREAL_1:1, XXREAL_1:4;
hence x in ].(- 1),s.[ /\ [.0 ,1.] by XBOOLE_0:def 4; :: thesis: verum

end;

then [.0 ,s.[ = ].(- 1),s.[ /\ [.0 ,1.] by A7, XBOOLE_0:def 10;
then A14: P2 = Q /\ ([#] (R^1 | T)) by A1, PRE_TOPC:def 10;
Closed-Interval-TSpace 0 ,1 = R^1 | T by TOPMETR:26;
hence P is open by A5, A14, TOPMETR:27, TOPS_2:32; :: thesis: verum

end;

suppose A15: not s in [.0 ,1.] ; :: thesis: P is open

now

per cases ( s < 0 or s > 1 ) by A15, XXREAL_1:1;

case s < 0 ; :: thesis: P is open

then [.0 ,s.[ = {} by XXREAL_1:27;
then P in the topology of I[01] by A1, PRE_TOPC:5;
hence P is open by PRE_TOPC:def 5; :: thesis: verum

end;

case s > 1 ; :: thesis: contradiction

then consider t being real number such that
A16: ( 1 < t & t < s ) by XREAL_1:7;
A17: for r being Real st 0 <= r & r < s holds
r <= 1

proof

let r be Real; :: thesis: ( 0 <= r & r < s implies r <= 1 )
assume ( 0 <= r & r < s ) ; :: thesis: r <= 1
then r in [.0 ,s.[ by XXREAL_1:3;
hence r <= 1 by A1, A2, XXREAL_1:1; :: thesis: verum

end;

reconsider t = t as Real by XREAL_0:def 1;
0 < t by A16;
hence contradiction by A16, A17; :: thesis: verum

end;

end;

end;

hence P is open ; :: thesis: verum

end;

end;