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,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) 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,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) 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,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B )

let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B )

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B ; :: thesis: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))

for x being Point of T

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

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) 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,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) 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,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B )

let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B )

hereby :: thesis: ( ( for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )

assume A7:
for B being Element of cB ex i, j being Nat st for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )

assume A1:
x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
; :: thesis: for B being Element of cB ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

end;for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

hereby :: thesis: verum

let B be Element of cB; :: thesis: ex i, j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

consider i, j being Nat such that

A2: s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) c= B by A1, Th52;

take i = i; :: thesis: ex j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

take j = j; :: thesis: for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

thus for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B :: thesis: verum

end;for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

consider i, j being Nat such that

A2: s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) c= B by A1, Th52;

take i = i; :: thesis: ex j being Nat st

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

take j = j; :: thesis: for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B

thus for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B :: thesis: verum

proof

let m, n be Nat; :: thesis: ( ( i <= m or j <= n ) implies s . (m,n) in B )

assume A3: ( i <= m or j <= n ) ; :: thesis: s . (m,n) in B

( m in NAT & n in NAT ) by ORDINAL1:def 12;

then A4: [m,n] in [:NAT,NAT:] by ZFMISC_1:def 2;

A5: ( not m in Segm i or not n in Segm j ) by A3, NAT_1:44;

not [m,n] in [:(Segm i),(Segm j):]

[m,n] in dom s by A4, FUNCT_2:def 1;

then s . [m,n] in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) by A6, FUNCT_1:def 6;

then s . [m,n] in B by A2;

hence s . (m,n) in B by BINOP_1:def 1; :: thesis: verum

end;assume A3: ( i <= m or j <= n ) ; :: thesis: s . (m,n) in B

( m in NAT & n in NAT ) by ORDINAL1:def 12;

then A4: [m,n] in [:NAT,NAT:] by ZFMISC_1:def 2;

A5: ( not m in Segm i or not n in Segm j ) by A3, NAT_1:44;

not [m,n] in [:(Segm i),(Segm j):]

proof

then A6:
[m,n] in [:NAT,NAT:] \ [:(Segm i),(Segm j):]
by A4, XBOOLE_0:def 5;
assume
[m,n] in [:(Segm i),(Segm j):]
; :: thesis: contradiction

then ex a, b being object st

( a in Segm i & b in Segm j & [m,n] = [a,b] ) by ZFMISC_1:def 2;

hence contradiction by A5, XTUPLE_0:1; :: thesis: verum

end;then ex a, b being object st

( a in Segm i & b in Segm j & [m,n] = [a,b] ) by ZFMISC_1:def 2;

hence contradiction by A5, XTUPLE_0:1; :: thesis: verum

[m,n] in dom s by A4, FUNCT_2:def 1;

then s . [m,n] in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) by A6, FUNCT_1:def 6;

then s . [m,n] in B by A2;

hence s . (m,n) in B by BINOP_1:def 1; :: thesis: verum

for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B ; :: thesis: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))

now :: thesis: for B being Element of cB ex n1, n2 being Nat st s .: ([:NAT,NAT:] \ [:(Segm n1),(Segm n2):]) c= B

hence
x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
by Th52; :: thesis: verumlet B be Element of cB; :: thesis: ex n1, n2 being Nat st s .: ([:NAT,NAT:] \ [:(Segm n1),(Segm n2):]) c= B

consider i, j being Nat such that

A8: for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B by A7;

s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) c= B

end;consider i, j being Nat such that

A8: for m, n being Nat st ( i <= m or j <= n ) holds

s . (m,n) in B by A7;

s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) c= B

proof

hence
ex n1, n2 being Nat st s .: ([:NAT,NAT:] \ [:(Segm n1),(Segm n2):]) c= B
; :: thesis: verum
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) or t in B )

assume t in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) ; :: thesis: t in B

then consider a being object such that

A9: a in dom s and

A10: a in [:NAT,NAT:] \ [:(Segm i),(Segm j):] and

A11: t = s . a by FUNCT_1:def 6;

reconsider a = a as Element of [:NAT,NAT:] by A9;

consider a1, a2 being object such that

A12: a1 in NAT and

A13: a2 in NAT and

A14: a = [a1,a2] by ZFMISC_1:def 2;

reconsider a1 = a1, a2 = a2 as Nat by A12, A13;

( not a1 in Segm i or not a2 in Segm j )

t = s . (a1,a2) by A11, A14, BINOP_1:def 1;

hence t in B by A8, A15; :: thesis: verum

end;assume t in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) ; :: thesis: t in B

then consider a being object such that

A9: a in dom s and

A10: a in [:NAT,NAT:] \ [:(Segm i),(Segm j):] and

A11: t = s . a by FUNCT_1:def 6;

reconsider a = a as Element of [:NAT,NAT:] by A9;

consider a1, a2 being object such that

A12: a1 in NAT and

A13: a2 in NAT and

A14: a = [a1,a2] by ZFMISC_1:def 2;

reconsider a1 = a1, a2 = a2 as Nat by A12, A13;

( not a1 in Segm i or not a2 in Segm j )

proof

then A15:
( i <= a1 or j <= a2 )
by NAT_1:44;
assume
( a1 in Segm i & a2 in Segm j )
; :: thesis: contradiction

then [a1,a2] in [:(Segm i),(Segm j):] by ZFMISC_1:def 2;

hence contradiction by A14, A10, XBOOLE_0:def 5; :: thesis: verum

end;then [a1,a2] in [:(Segm i),(Segm j):] by ZFMISC_1:def 2;

hence contradiction by A14, A10, XBOOLE_0:def 5; :: thesis: verum

t = s . (a1,a2) by A11, A14, BINOP_1:def 1;

hence t in B by A8, A15; :: thesis: verum