let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n)
for a, b being real number
for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } & i in Seg n holds
P is open
let P be Subset of (TOP-REAL n); :: thesis: for a, b being real number
for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } & i in Seg n holds
P is open
let a, b be real number ; :: thesis: for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } & i in Seg n holds
P is open
let i be Element of NAT ; :: thesis: ( P = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } & i in Seg n implies P is open )
assume A1: ( P = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } & i in Seg n ) ; :: thesis: P is open
A2: P = { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b }

proof

A3: P c= { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } )
assume x in P ; :: thesis: x in { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b }
then consider p3 being Point of (TOP-REAL n) such that
A4: ( p3 = x & a < Proj p3,i & Proj p3,i < b ) by A1;
( x in { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } & x in { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } ) by A4;
hence x in { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } by XBOOLE_0:def 4; :: thesis: verum

end;

{ p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } or x in P )
assume x in { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } ; :: thesis: x in P
then A5: ( x in { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } & x in { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } ) by XBOOLE_0:def 4;
then consider p1 being Point of (TOP-REAL n) such that
A6: ( x = p1 & a < Proj p1,i ) ;
consider p2 being Point of (TOP-REAL n) such that
A7: ( x = p2 & Proj p2,i < b ) by A5;
thus x in P by A1, A6, A7; :: thesis: verum

end;

hence P = { p1 where p1 is Point of (TOP-REAL n) : a < Proj p1,i } /\ { p2 where p2 is Point of (TOP-REAL n) : Proj p2,i < b } by A3, XBOOLE_0:def 10; :: thesis: verum

end;

{ p where p is Point of (TOP-REAL n) : a < Proj p,i } c= the carrier of (TOP-REAL n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL n) : a < Proj p,i } or x in the carrier of (TOP-REAL n) )
assume x in { p where p is Point of (TOP-REAL n) : a < Proj p,i } ; :: thesis: x in the carrier of (TOP-REAL n)
then consider p being Point of (TOP-REAL n) such that
A8: ( x = p & a < Proj p,i ) ;
thus x in the carrier of (TOP-REAL n) by A8; :: thesis: verum

end;

then reconsider P1 = { p where p is Point of (TOP-REAL n) : a < Proj p,i } as Subset of (TOP-REAL n) ;
{ p where p is Point of (TOP-REAL n) : Proj p,i < b } c= the carrier of (TOP-REAL n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL n) : Proj p,i < b } or x in the carrier of (TOP-REAL n) )
assume x in { p where p is Point of (TOP-REAL n) : Proj p,i < b } ; :: thesis: x in the carrier of (TOP-REAL n)
then consider p being Point of (TOP-REAL n) such that
A9: ( x = p & Proj p,i < b ) ;
thus x in the carrier of (TOP-REAL n) by A9; :: thesis: verum

end;

then reconsider P2 = { p where p is Point of (TOP-REAL n) : Proj p,i < b } as Subset of (TOP-REAL n) ;
A10: P1 is open by A1, Th17;
P2 is open by A1, Th16;
hence P is open by A2, A10, TOPS_1:38; :: thesis: verum