A1: [#] I[01] = [.0,1.] by TOPMETR:18, TOPMETR:20;
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 A2: P = ].s,1.] ; :: thesis: P is open
per cases ( s in [.0,1.] or not s in [.0,1.] ) ;
suppose A3: s in [.0,1.] ; :: thesis: P is open
reconsider T = [.0,1.] as Subset of R^1 by TOPMETR:17;
1 in [.0,1.] by XXREAL_1:1;
then ( ].s,1.] c= [.s,1.] & [.s,1.] c= [.0,1.] ) by A3, XXREAL_1:23, XXREAL_2:def 12;
then ].s,1.] c= [.0,1.] ;
then P c= [#] (R^1 | T) by A2, PRE_TOPC:def 5;
then reconsider P2 = P as Subset of (R^1 | T) ;
reconsider Q = ].s,2.[ as Subset of R^1 by TOPMETR:17;
A4: 0 <= s by A3, XXREAL_1:1;
A5: ].s,1.] c= ].s,2.[ /\ [.0,1.]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].s,1.] or x in ].s,2.[ /\ [.0,1.] )
assume A6: x in ].s,1.] ; :: thesis: x in ].s,2.[ /\ [.0,1.]
then reconsider sx = x as Real ;
A7: s < sx by A6, XXREAL_1:2;
A8: sx <= 1 by A6, XXREAL_1:2;
then 2 > sx by XXREAL_0:2;
then A9: x in ].s,2.[ by A7, XXREAL_1:4;
x in [.0,1.] by A4, A7, A8, XXREAL_1:1;
hence x in ].s,2.[ /\ [.0,1.] by A9, XBOOLE_0:def 4; :: thesis: verum
end;
].s,2.[ /\ [.0,1.] c= ].s,1.]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].s,2.[ /\ [.0,1.] or x in ].s,1.] )
assume A10: x in ].s,2.[ /\ [.0,1.] ; :: thesis: x in ].s,1.]
then reconsider sx = x as Real ;
x in [.0,1.] by A10, XBOOLE_0:def 4;
then A11: sx <= 1 by XXREAL_1:1;
x in ].s,2.[ by A10, XBOOLE_0:def 4;
then s < sx by XXREAL_1:4;
hence x in ].s,1.] by A11, XXREAL_1:2; :: thesis: verum
end;
then ].s,1.] = ].s,2.[ /\ [.0,1.] by A5, XBOOLE_0:def 10;
then A12: P2 = Q /\ ([#] (R^1 | T)) by A2, PRE_TOPC:def 5;
( Q is open & Closed-Interval-TSpace (0,1) = R^1 | T ) by JORDAN6:35, TOPMETR:19;
hence P is open by A12, TOPMETR:20, TOPS_2:24; :: thesis: verum
end;
suppose A13: not s in [.0,1.] ; :: thesis: P is open
now :: thesis: ( ( s > 1 & P is open ) or ( s < 0 & contradiction ) )
per cases ( s > 1 or s < 0 ) by A13, XXREAL_1:1;
case A14: s < 0 ; :: thesis: contradiction
A15: 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 A2, A1, XXREAL_1:1; :: thesis: verum
end;
consider t being Real such that
A16: s < t and
A17: t < 0 by A14, XREAL_1:5;
reconsider t = t as Real ;
thus contradiction by A16, A17, A15; :: thesis: verum
end;
end;
end;
hence P is open ; :: thesis: verum
end;
end;