let m, n be Nat; :: thesis: for s being Function of ,()
for y being Point of () holds
( s .: () c= { q where q is Element of () : dist (y,q) < 1 / m } iff for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )

let s be Function of ,(); :: thesis: for y being Point of () holds
( s .: () c= { q where q is Element of () : dist (y,q) < 1 / m } iff for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )

let y be Point of (); :: thesis: ( s .: () c= { q where q is Element of () : dist (y,q) < 1 / m } iff for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )

hereby :: thesis: ( ( for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) ) implies s .: () c= { q where q is Element of () : dist (y,q) < 1 / m } )
assume A1: s .: () c= { q where q is Element of () : dist (y,q) < 1 / m } ; :: thesis: for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m )

now :: thesis: for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m )
let x be object ; :: thesis: ( x in s .: () implies ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )

assume A2: x in s .: () ; :: thesis: ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m )

then consider yo being object such that
A3: yo in dom s and
yo in square-uparrow n and
A4: x = s . yo by FUNCT_1:def 6;
reconsider z = x as Element of () by ;
z in { q where q is Element of () : dist (y,q) < 1 / m } by A2, A1;
then consider q being Element of () such that
A5: z = q and
A6: dist (y,q) < 1 / m ;
reconsider yr1 = y as Point of () ;
yr1 in 1 -tuples_on REAL ;
then yr1 in { <*r*> where r is Element of REAL : verum } by FINSEQ_2:96;
then consider ry being Element of REAL such that
A8: yr1 = <*ry*> ;
reconsider zr1 = z as Point of () ;
zr1 in 1 -tuples_on REAL ;
then zr1 in { <*r*> where r is Element of REAL : verum } by FINSEQ_2:96;
then consider rx being Element of REAL such that
A9: zr1 = <*rx*> ;
|.(ry - rx).| < 1 / m by A5, A6, A8, A9, Th8;
hence ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) by A8, A9; :: thesis: verum
end;
hence for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) ; :: thesis: verum
end;
assume A10: for x being object st x in s .: () holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) ; :: thesis: s .: () c= { q where q is Element of () : dist (y,q) < 1 / m }
now :: thesis: for t being object st t in s .: () holds
t in { q where q is Element of () : dist (y,q) < 1 / m }
let t be object ; :: thesis: ( t in s .: () implies t in { q where q is Element of () : dist (y,q) < 1 / m } )
assume A11: t in s .: () ; :: thesis: t in { q where q is Element of () : dist (y,q) < 1 / m }
then consider rx, ry being Real such that
A12: t = <*rx*> and
A13: y = <*ry*> and
A14: |.(ry - rx).| < 1 / m by A10;
consider yo being object such that
A15: yo in dom s and
yo in square-uparrow n and
A16: t = s . yo by ;
reconsider q = t as Element of () by ;
dist (y,q) < 1 / m by A12, A13, A14, Th8;
hence t in { q where q is Element of () : dist (y,q) < 1 / m } ; :: thesis: verum
end;
hence s .: () c= { q where q is Element of () : dist (y,q) < 1 / m } ; :: thesis: verum