let P be Subset of I[01] ; :: thesis: for s being Real st P = ].s,1.] holds
P is open
let s be Real; :: thesis: ( P = ].s,1.] implies P is open )
assume A1: P = ].s,1.] ; :: 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 = ].s,2.[ 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: ].s,1.] c= [.s,1.] by XXREAL_1:23;
1 in [.0 ,1.] by XXREAL_1:1;
then [.s,1.] c= [.0 ,1.] by A3, XXREAL_2:def 12;
then ].s,1.] 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: ].s,2.[ /\ [.0 ,1.] c= ].s,1.]

proof

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

end;

].s,1.] c= ].s,2.[ /\ [.0 ,1.]

proof

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

end;

then ].s,1.] = ].s,2.[ /\ [.0 ,1.] by A7, XBOOLE_0:def 10;
then A13: 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, A13, TOPMETR:27, TOPS_2:32; :: thesis: verum

end;

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

now

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

case s > 1 ; :: thesis: P is open

then ].s,1.] = {} by XXREAL_1:26;
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 < 0 ; :: thesis: contradiction

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

proof

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

end;

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

end;

end;

end;

hence P is open ; :: thesis: verum

end;

end;