let P be Subset of R^1; :: thesis: for a, b being real number st P = { s where s is Real : ( a < s & s < b ) } holds
P is open
let a, b be real number ; :: 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 set ; :: 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 ex r1 being Real st
( x = r1 & a < r1 ) ;
hence x in the carrier of R^1 by TOPMETR:17; :: 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 set ; :: 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 ex r2 being Real st
( x = r2 & r2 < b ) ;
hence x in the carrier of R^1 by TOPMETR:17; :: thesis: verum

end;

then reconsider P2 = { w2 where w2 is Real : w2 < b } as Subset of R^1 ;
assume A1: P = { s where s is Real : ( a < s & s < b ) } ; :: thesis: P is open
A2: P = { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b }

proof

A3: { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } c= P

proof

let x be set ; :: 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 A4: 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 A5: ex r2 being Real st
( x = r2 & r2 < b ) ;
x in { w1 where w1 is Real : a < w1 } by A4, XBOOLE_0:def 4;
then ex r1 being Real st
( x = r1 & a < r1 ) ;
hence x in P by A1, A5; :: thesis: verum

end;

P c= { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b }

proof

let x be set ; :: 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 A6: ex s being Real st
( s = x & a < s & s < b ) by A1;
then A7: x in { w2 where w2 is Real : w2 < b } ;
x in { w1 where w1 is Real : a < w1 } by A6;
hence x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } by A7, XBOOLE_0:def 4; :: thesis: verum

end;

hence P = { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } by A3, XBOOLE_0:def 10; :: thesis: verum

end;

( P1 is open & P2 is open ) by Th30, Th31;
hence P is open by A2, TOPS_1:11; :: thesis: verum