set T = TopSpaceMetr (Euclid n);
OpenHypercube (e,(1 / 1)) in OpenHypercubes e ;
hence not OpenHypercubes e is empty ; :: thesis: ( OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis )

hereby :: according to TOPS_2:def 1 :: thesis: OpenHypercubes e is @ e -quasi_basis

let A be Subset of (TopSpaceMetr (Euclid n)); :: 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 (OpenHypercubes e) by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b₁ being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) holds
( not b₁ is open or not @ e in b₁ or ex b₂ being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st
( b₂ in OpenHypercubes e & b₂ c= b₁ ) )
let S be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( not S is open or not @ e in S or ex b₁ being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st
( b₁ in OpenHypercubes e & b₁ c= S ) )
assume that
A1: S is open and
A2: @ e in S ; :: thesis: ex b₁ being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st
( b₁ in OpenHypercubes e & b₁ c= S )
consider r being Real such that
A3: r > 0 and
A4: Ball (e,r) c= S by A1, A2, TOPMETR:15;
consider m being non zero Element of NAT such that
A5: OpenHypercube (e,(1 / m)) c= Ball (e,r) by A3, Th19, GOBOARD6:1;
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