let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n)
for a, b being Real
for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & 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
for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } & i in Seg n holds
P is open
let a, b be Real; :: thesis: for i being Element of NAT st P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & 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 < p /. i & p /. i < b ) } & i in Seg n implies P is open )
assume that
A1: P = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } and
A2: i in Seg n ; :: thesis: P is open
A3: P = { p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i } /\ { p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b }

proof

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

proof

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

end;

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

proof

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

end;

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

end;

{ p where p is Point of (TOP-REAL n) : p /. i < b } c= the carrier of (TOP-REAL n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL n) : p /. i < b } or x in the carrier of (TOP-REAL n) )
assume x in { p where p is Point of (TOP-REAL n) : p /. i < b } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex p being Point of (TOP-REAL n) st
( x = p & p /. i < b ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL n) : a < p /. i } or x in the carrier of (TOP-REAL n) )
assume x in { p where p is Point of (TOP-REAL n) : a < p /. i } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex p being Point of (TOP-REAL n) st
( x = p & a < p /. i ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P1 = { p where p is Point of (TOP-REAL n) : a < p /. i } as Subset of (TOP-REAL n) ;
( P1 is open & P2 is open ) by A2, Th12, Th13;
hence P is open by A3, TOPS_1:11; :: thesis: verum