let n be Nat; :: thesis: for O being non empty open Subset of (TOP-REAL n) ex s being sequence of (dense_countable_OpenHypercubes n) st O = Union s
let O be non empty open Subset of (TOP-REAL n); :: thesis: ex s being sequence of (dense_countable_OpenHypercubes n) st O = Union s
consider s being sequence of (dense_countable_OpenHypercubes n) such that
A1: for x being object holds
( x in O iff ex y being object st
( y in NAT & x in s . y ) ) by Th25;
A2: dom s = NAT by FUNCT_2:def 1;
take s ; :: thesis: O = Union s

now :: thesis: for x being object holds
( ( x in O implies x in Union s ) & ( x in Union s implies x in O ) )

let x be object ; :: thesis: ( ( x in O implies x in Union s ) & ( x in Union s implies x in O ) )

hereby :: thesis: ( x in Union s implies x in O )

assume x in O ; :: thesis: x in Union s
then consider y being object such that
A3: y in NAT and
A4: x in s . y by A1;
s . y in rng s by A3, A2, FUNCT_1:def 3;
hence x in Union s by A4, TARSKI:def 4; :: thesis: verum

end;

assume x in Union s ; :: thesis: x in O
then consider y being set such that
A5: x in y and
A6: y in rng s by TARSKI:def 4;
consider z being object such that
A7: z in dom s and
A8: y = s . z by A6, FUNCT_1:def 3;
thus x in O by A1, A5, A7, A8; :: thesis: verum

end;

hence O = Union s by TARSKI:2; :: thesis: verum