theorem :: CARDFIL4:70

for m, n being Nat
for s being Function of [:NAT,NAT:],(TopSpaceMetr (Euclid 1))
for y being Point of (Euclid 1) holds
( s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } iff for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )