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

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