set T = TopSpaceMetr ();
OpenHypercube (e,(1 / 1)) in OpenHypercubes e ;
hence not OpenHypercubes e is empty ; :: thesis:
hereby :: according to TOPS_2:def 1 :: thesis:
let A be Subset of (); :: thesis: ( A in OpenHypercubes e implies A is open )
assume A in OpenHypercubes e ; :: thesis: A is open
then ex m being non zero Element of NAT st A = OpenHypercube (e,(1 / m)) ;
hence A is open ; :: thesis: verum
end;
now :: thesis: for Y being set st Y in OpenHypercubes e holds
@ e in Y
let Y be set ; :: thesis: ( Y in OpenHypercubes e implies @ e in Y )
assume Y in OpenHypercubes e ; :: thesis: @ e in Y
then ex m being non zero Element of NAT st Y = OpenHypercube (e,(1 / m)) ;
hence @ e in Y by Th11; :: thesis: verum
end;
hence @ e in Intersect () by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b1 being Element of K19( the carrier of ()) holds
( not b1 is open or not @ e in b1 or ex b2 being Element of K19( the carrier of ()) st
( b2 in OpenHypercubes e & b2 c= b1 ) )

let S be Subset of (); :: thesis: ( not S is open or not @ e in S or ex b1 being Element of K19( the carrier of ()) st
( b1 in OpenHypercubes e & b1 c= S ) )

assume that
A1: S is open and
A2: @ e in S ; :: thesis: ex b1 being Element of K19( the carrier of ()) st
( b1 in OpenHypercubes e & b1 c= S )

consider r being Real such that
A3: r > 0 and
A4: Ball (e,r) c= S by ;
consider m being non zero Element of NAT such that
A5: OpenHypercube (e,(1 / m)) c= Ball (e,r) by ;
take V = OpenHypercube (e,(1 / m)); :: thesis: ( V in OpenHypercubes e & V c= S )
thus V in OpenHypercubes e ; :: thesis: V c= S
thus V c= S by A4, A5; :: thesis: verum