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 ) )

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 }

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 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 ) ) 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 )

ex rx, ry being Real st

( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) ; :: thesis: verum

end;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 )

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 )

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;( 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

ex rx, ry being Real st

( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) ; :: thesis: verum

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 }

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