let m, n be Nat; :: thesis: 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 ) )
let s be Function of [:NAT,NAT:],(TopSpaceMetr (Euclid 1)); :: thesis: 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 ) )
let y be Point of (Euclid 1); :: thesis: ( 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 ) )

hereby :: thesis: ( ( 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 ) ) implies s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } )

assume A1: s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } ; :: thesis: 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 )

now :: thesis: 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 )

let x be object ; :: thesis: ( x in s .: (square-uparrow n) implies ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )
assume A2: x in s .: (square-uparrow n) ; :: 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 (Euclid 1) by A3, A4, FUNCT_2:5;
z in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } by A2, A1;
then consider q being Element of (Euclid 1) such that
A5: z = q and
A6: dist (y,q) < 1 / m ;
reconsider yr1 = y as Point of (Euclid 1) ;
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 (Euclid 1) ;
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 .: (square-uparrow n) 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 .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) ; :: thesis: s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m }

now :: thesis: for t being object st t in s .: (square-uparrow n) holds
t in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m }

let t be object ; :: thesis: ( t in s .: (square-uparrow n) implies t in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } )
assume A11: t in s .: (square-uparrow n) ; :: thesis: t in { q where q is Element of (Euclid 1) : 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 A11, FUNCT_1:def 6;
reconsider q = t as Element of (Euclid 1) by A15, A16, FUNCT_2:5;
dist (y,q) < 1 / m by A12, A13, A14, Th8;
hence t in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } ; :: thesis: verum

end;

hence s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } ; :: thesis: verum