let n be Nat; :: thesis:
let O be non empty open Subset of (TOP-REAL n); :: thesis:
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:

assume x in O ; :: thesis:
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:

end;

assume x in Union s ; :: thesis:
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:

end;