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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) 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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) 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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) 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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B )

for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite

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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) 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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) 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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) 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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B )

hereby :: thesis: ( ( for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )

assume A3:
for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) 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 A being finite Subset of [:NAT,NAT:] st s .: ([:NAT,NAT:] \ A) c= B

end;hereby :: thesis: verum

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

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

A2: s " B = [:NAT,NAT:] \ A by A1, Th49;

take A = A; :: thesis: s .: ([:NAT,NAT:] \ A) c= B

thus s .: ([:NAT,NAT:] \ A) c= B by A2, FUNCT_1:75; :: thesis: verum

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

A2: s " B = [:NAT,NAT:] \ A by A1, Th49;

take A = A; :: thesis: s .: ([:NAT,NAT:] \ A) c= B

thus s .: ([:NAT,NAT:] \ A) c= B by A2, FUNCT_1:75; :: thesis: verum

for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite

proof

hence
x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
by Th46; :: thesis: verum
let A be a_neighborhood of x; :: thesis: [:NAT,NAT:] \ (s " A) is finite

A4: A is Element of BOOL2F (NeighborhoodSystem x) by YELLOW19:2;

cB is filter_basis ;

then consider B being Element of cB such that

A5: B c= A by A4;

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

A6: s .: ([:NAT,NAT:] \ C) c= B by A3;

s .: ([:NAT,NAT:] \ C) c= A by A6, A5;

then A7: s " (s .: ([:NAT,NAT:] \ C)) c= s " A by RELAT_1:143;

dom s = [:NAT,NAT:] by FUNCT_2:def 1;

then [:NAT,NAT:] \ C c= s " (s .: ([:NAT,NAT:] \ C)) by FUNCT_1:76;

then [:NAT,NAT:] \ C c= s " A by A7;

then [:NAT,NAT:] \ (s " A) c= [:NAT,NAT:] \ ([:NAT,NAT:] \ C) by XBOOLE_1:34;

then [:NAT,NAT:] \ (s " A) c= [:NAT,NAT:] /\ C by XBOOLE_1:48;

hence [:NAT,NAT:] \ (s " A) is finite ; :: thesis: verum

end;A4: A is Element of BOOL2F (NeighborhoodSystem x) by YELLOW19:2;

cB is filter_basis ;

then consider B being Element of cB such that

A5: B c= A by A4;

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

A6: s .: ([:NAT,NAT:] \ C) c= B by A3;

s .: ([:NAT,NAT:] \ C) c= A by A6, A5;

then A7: s " (s .: ([:NAT,NAT:] \ C)) c= s " A by RELAT_1:143;

dom s = [:NAT,NAT:] by FUNCT_2:def 1;

then [:NAT,NAT:] \ C c= s " (s .: ([:NAT,NAT:] \ C)) by FUNCT_1:76;

then [:NAT,NAT:] \ C c= s " A by A7;

then [:NAT,NAT:] \ (s " A) c= [:NAT,NAT:] \ ([:NAT,NAT:] \ C) by XBOOLE_1:34;

then [:NAT,NAT:] \ (s " A) c= [:NAT,NAT:] /\ C by XBOOLE_1:48;

hence [:NAT,NAT:] \ (s " A) is finite ; :: thesis: verum