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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= 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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= 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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= 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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B )

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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= 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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= 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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= 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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B )

hereby :: thesis: ( ( for B being Element of cB ex n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )

assume A4:
for B being Element of cB ex n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B
; :: thesis: 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 n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B

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

hence
for B being Element of cB ex n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B
; :: thesis: verumlet B be Element of cB; :: thesis: ex n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B

consider A being finite Subset of [:NAT,NAT:] such that

A2: s .: ([:NAT,NAT:] \ A) c= B by A1, Th51;

consider n, m being Nat such that

A3: A c= [:(Segm n),(Segm m):] by Th16;

[:NAT,NAT:] \ [:(Segm n),(Segm m):] c= [:NAT,NAT:] \ A by A3, XBOOLE_1:34;

then s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= s .: ([:NAT,NAT:] \ A) by RELAT_1:123;

then s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B by A2;

hence ex n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B ; :: thesis: verum

end;consider A being finite Subset of [:NAT,NAT:] such that

A2: s .: ([:NAT,NAT:] \ A) c= B by A1, Th51;

consider n, m being Nat such that

A3: A c= [:(Segm n),(Segm m):] by Th16;

[:NAT,NAT:] \ [:(Segm n),(Segm m):] c= [:NAT,NAT:] \ A by A3, XBOOLE_1:34;

then s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= s .: ([:NAT,NAT:] \ A) by RELAT_1:123;

then s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B by A2;

hence ex n, m being Nat st s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B ; :: thesis: verum

now :: thesis: for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B

hence
x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
by Th51; :: thesis: verumlet B be Element of cB; :: thesis: ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B

consider n, m being Nat such that

A5: s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B by A4;

reconsider A = [:(Segm n),(Segm m):] as finite Subset of [:NAT,NAT:] ;

thus ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B by A5; :: thesis: verum

end;consider n, m being Nat such that

A5: s .: ([:NAT,NAT:] \ [:(Segm n),(Segm m):]) c= B by A4;

reconsider A = [:(Segm n),(Segm m):] as finite Subset of [:NAT,NAT:] ;

thus ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B by A5; :: thesis: verum