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 )
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: 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 consider s being Real such that
A4: ( s = x & a < s & s < b ) by A1;
( x in { w1 where w1 is Real : a < w1 } & x in { w2 where w2 is Real : w2 < b } ) by A4;
hence x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } by XBOOLE_0:def 4; :: thesis: verum

end;

{ 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 x in { w1 where w1 is Real : a < w1 } /\ { w2 where w2 is Real : w2 < b } ; :: thesis: x in P
then A5: ( x in { w1 where w1 is Real : a < w1 } & x in { w2 where w2 is Real : w2 < b } ) by XBOOLE_0:def 4;
then consider r1 being Real such that
A6: ( x = r1 & a < r1 ) ;
ex r2 being Real st
( x = r2 & r2 < b ) by A5;
then consider r2 being real number such that
A7: ( x = r2 & r2 < b ) ;
thus x in P by A1, A6, A7; :: 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;

{ 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 consider r1 being Real such that
A8: ( x = r1 & a < r1 ) ;
thus x in the carrier of R^1 by A8, TOPMETR:24; :: 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 consider r2 being Real such that
A9: ( x = r2 & r2 < b ) ;
thus x in the carrier of R^1 by A9, TOPMETR:24; :: thesis: verum

end;

then reconsider P2 = { w2 where w2 is Real : w2 < b } as Subset of R^1 ;
A10: P1 is open by Th31;
P2 is open by Th30;
hence P is open by A2, A10, TOPS_1:38; :: thesis: verum