let n be Nat; :: thesis: for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds
for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V
let V be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( V is open implies for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V )
assume A1: V is open ; :: thesis: for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V
let e be Point of (Euclid n); :: thesis: ( e in V implies ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V )
assume e in V ; :: thesis: ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V
then consider r being Real such that
A2: r > 0 and
A3: Ball (e,r) c= V by A1, TOPMETR:15;
consider m being non zero Element of NAT such that
A4: OpenHypercube (e,(1 / m)) c= Ball (e,r) by A2, Th19, GOBOARD6:1;
take m ; :: thesis: OpenHypercube (e,(1 / m)) c= V
thus OpenHypercube (e,(1 / m)) c= V by A3, A4; :: thesis: verum