let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T

for x being Point of T

for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for x being Point of T

for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

let x be Point of T; :: thesis: for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

( ( for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B ) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ) by Th50; :: thesis: verum

for x being Point of T

for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for x being Point of T

for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

let x be Point of T; :: thesis: for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

( ( for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B ) iff for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B )

proof

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ; :: thesis: for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B

end;

hence
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st hereby :: thesis: ( ( for B being Element of cB ex n being Nat st

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ) implies for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B )

assume A3:
for B being Element of cB ex n being Nat st for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ) implies for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B )

assume A1:
for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B
; :: thesis: for B being Element of cB ex n0 being Nat st

for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B

end;for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B

hereby :: thesis: verum

let B be Element of cB; :: thesis: ex n0 being Nat st

for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B

consider n0 being Nat such that

A2: s .: (square-uparrow n0) c= B by A1;

take n0 = n0; :: thesis: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B

thus for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B by A2, Th53; :: thesis: verum

end;for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B

consider n0 being Nat such that

A2: s .: (square-uparrow n0) c= B by A1;

take n0 = n0; :: thesis: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B

thus for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B by A2, Th53; :: thesis: verum

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ; :: thesis: for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B

hereby :: thesis: verum

let B be Element of cB; :: thesis: ex n being Nat st s .: (square-uparrow n) c= B

consider n0 being Nat such that

A4: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B by A3;

thus ex n being Nat st s .: (square-uparrow n) c= B :: thesis: verum

end;consider n0 being Nat such that

A4: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds

s . (n1,n2) in B by A3;

thus ex n being Nat st s .: (square-uparrow n) c= B :: thesis: verum

proof

take
n0
; :: thesis: s .: (square-uparrow n0) c= B

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s .: (square-uparrow n0) or x in B )

assume x in s .: (square-uparrow n0) ; :: thesis: x in B

then ex n1, n2 being Nat st

( n0 <= n1 & n0 <= n2 & x = s . (n1,n2) ) by Th53;

hence x in B by A4; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s .: (square-uparrow n0) or x in B )

assume x in s .: (square-uparrow n0) ; :: thesis: x in B

then ex n1, n2 being Nat st

( n0 <= n1 & n0 <= n2 & x = s . (n1,n2) ) by Th53;

hence x in B by A4; :: thesis: verum

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ) by Th50; :: thesis: verum