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 b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) holds
( not b1 is open or not @ e in b1 or ex b2 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st
( b2 in OpenHypercubes e & b2 c= b1 ) )
let S be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( not S is open or not @ e in S or ex b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) 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 (TopSpaceMetr (Euclid n))) 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 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