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 number such that
A2: r > 0 and
A3: Ball e,r c= V by A1, TOPMETR:22;
consider m being non zero Element of NAT such that
A4: OpenHypercube e,(1 / m) c= Ball e,r by A2, GOBOARD6:4, Th19;
take m ; :: thesis: OpenHypercube e,(1 / m) c= V
thus OpenHypercube e,(1 / m) c= V by A3, A4, XBOOLE_1:1; :: thesis: verum