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 )

_{1} being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) holds

( not b_{1} is open or not @ e in b_{1} or ex b_{2} being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st

( b_{2} in OpenHypercubes e & b_{2} c= b_{1} ) )

let S be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( not S is open or not @ e in S or ex b_{1} being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st

( b_{1} in OpenHypercubes e & b_{1} c= S ) )

assume that

A1: S is open and

A2: @ e in S ; :: thesis: ex b_{1} being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st

( b_{1} in OpenHypercubes e & b_{1} 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

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;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

now :: thesis: for Y being set st Y in OpenHypercubes e holds

@ e in Y

hence
@ e in Intersect (OpenHypercubes e)
by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b@ 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;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

( not b

( b

let S be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( not S is open or not @ e in S or ex b

( b

assume that

A1: S is open and

A2: @ e in S ; :: thesis: ex b

( b

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