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

for x being Point of T holds

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

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

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

let x be Point of T; :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

set F = filter_image (s,(Frechet_Filter [:NAT,NAT:]));

A1: ( filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

for x being Point of T holds

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

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

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

let x be Point of T; :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

set F = filter_image (s,(Frechet_Filter [:NAT,NAT:]));

A1: ( filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )

proof

NeighborhoodSystem x c= filter_image (s,(Frechet_Filter [:NAT,NAT:]))

end;

( filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x iff x in lim_filter (filter_image (s,(Frechet_Filter [:NAT,NAT:]))) )
hereby :: thesis: ( ( for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B ) implies filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x )

assume A3:
for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B
; :: thesis: filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem xassume
filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x
; :: thesis: for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B

then NeighborhoodSystem x c= { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } by Th43;

then A2: { A where A is a_neighborhood of x : verum } c= { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } by YELLOW19:def 1;

thus for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B :: thesis: verum

end;then NeighborhoodSystem x c= { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } by Th43;

then A2: { A where A is a_neighborhood of x : verum } c= { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } by YELLOW19:def 1;

thus for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B :: thesis: verum

proof

let A be a_neighborhood of x; :: thesis: ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B

A in { A where A is a_neighborhood of x : verum } ;

then A in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } by A2;

then ex M being Subset of the carrier of T st

( A = M & ex B being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ B ) ;

hence ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B ; :: thesis: verum

end;A in { A where A is a_neighborhood of x : verum } ;

then A in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } by A2;

then ex M being Subset of the carrier of T st

( A = M & ex B being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ B ) ;

hence ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B ; :: thesis: verum

NeighborhoodSystem x c= filter_image (s,(Frechet_Filter [:NAT,NAT:]))

proof

hence
filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x
; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in NeighborhoodSystem x or y in filter_image (s,(Frechet_Filter [:NAT,NAT:])) )

assume y in NeighborhoodSystem x ; :: thesis: y in filter_image (s,(Frechet_Filter [:NAT,NAT:]))

then y in { A where A is a_neighborhood of x : verum } by YELLOW19:def 1;

then consider A being a_neighborhood of x such that

A4: y = A ;

ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B by A3;

then A in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } ;

hence y in filter_image (s,(Frechet_Filter [:NAT,NAT:])) by A4, Th43; :: thesis: verum

end;assume y in NeighborhoodSystem x ; :: thesis: y in filter_image (s,(Frechet_Filter [:NAT,NAT:]))

then y in { A where A is a_neighborhood of x : verum } by YELLOW19:def 1;

then consider A being a_neighborhood of x such that

A4: y = A ;

ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B by A3;

then A in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } ;

hence y in filter_image (s,(Frechet_Filter [:NAT,NAT:])) by A4, Th43; :: thesis: verum

proof

hence
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B )
by A1; :: thesis: verum
thus
( filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x implies x in lim_filter (filter_image (s,(Frechet_Filter [:NAT,NAT:]))) )
; :: thesis: ( x in lim_filter (filter_image (s,(Frechet_Filter [:NAT,NAT:]))) implies filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x )

assume x in lim_filter (filter_image (s,(Frechet_Filter [:NAT,NAT:]))) ; :: thesis: filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x

then ex y being Point of T st

( x = y & filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem y ) ;

hence filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x ; :: thesis: verum

end;assume x in lim_filter (filter_image (s,(Frechet_Filter [:NAT,NAT:]))) ; :: thesis: filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x

then ex y being Point of T st

( x = y & filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem y ) ;

hence filter_image (s,(Frechet_Filter [:NAT,NAT:])) is_filter-finer_than NeighborhoodSystem x ; :: thesis: verum