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