let P be Subset of R^1; :: thesis: for a, b being Real st P = { s where s is Real : ( a < s & s < b ) } holds
P is open
let a, b be Real; :: thesis: ( P = { s where s is Real : ( a < s & s < b ) } implies P is open )
{ w1 where w1 is Real : a < w1 } c= the carrier of R^1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w1 where w1 is Real : a < w1 } or x in the carrier of R^1 )
assume x in { w1 where w1 is Real : a < w1 } ; :: thesis: x in the carrier of R^1
then consider r1 being Real such that
A1: ( x = r1 & a < r1 ) ;
r1 in REAL by XREAL_0:def 1;
hence x in the carrier of R^1 by TOPMETR:17, A1; :: thesis: verum
end;
then reconsider P1 = { w1 where w1 is Real : a < w1 } as Subset of R^1 ;
{ w2 where w2 is Real : w2 < b } c= the carrier of R^1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w2 where w2 is Real : w2 < b } or x in the carrier of R^1 )
assume x in { w2 where w2 is Real : w2 < b } ; :: thesis: x in the carrier of R^1
then consider r2 being Real such that
A2: ( x = r2 & r2 < b ) ;
r2 in REAL by XREAL_0:def 1;
hence x in the carrier of R^1 by TOPMETR:17, A2; :: thesis: verum
end;
then reconsider P2 = { w2 where w2 is Real : w2 < b } as Subset of R^1 ;
assume A3: P = { s where s is Real : ( a < s & s < b ) } ; :: thesis: P is open
A4: P = { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b }
proof
A5: { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } c= P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } or x in P )
assume A6: x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } ; :: thesis: x in P
then x in { w2 where w2 is Real : w2 < b } by XBOOLE_0:def 4;
then A7: ex r2 being Real st
( x = r2 & r2 < b ) ;
x in { w1 where w1 is Real : a < w1 } by A6, XBOOLE_0:def 4;
then ex r1 being Real st
( x = r1 & a < r1 ) ;
hence x in P by A3, A7; :: thesis: verum
end;
P c= { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } )
assume x in P ; :: thesis: x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b }
then A8: ex s being Real st
( s = x & a < s & s < b ) by A3;
then A9: x in { w2 where w2 is Real : w2 < b } ;
x in { w1 where w1 is Real : a < w1 } by A8;
hence x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } by A9, XBOOLE_0:def 4; :: thesis: verum
end;
hence P = { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } by A5, XBOOLE_0:def 10; :: thesis: verum
end;
( P1 is open & P2 is open ) by Th24, Th25;
hence P is open by A4, TOPS_1:11; :: thesis: verum