let X be non empty set ; for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for F being Filter of X
for B being basis of F st [#] L is directed holds
( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) )
let L be non empty reflexive transitive RelStr ; for f being Function of ([#] L),X
for F being Filter of X
for B being basis of F st [#] L is directed holds
( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) )
let f be Function of ([#] L),X; for F being Filter of X
for B being basis of F st [#] L is directed holds
( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) )
let F be Filter of X; for B being basis of F st [#] L is directed holds
( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) )
let B be basis of F; ( [#] L is directed implies ( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) ) )
assume
[#] L is directed
; ( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) )
then
f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L)))
by Th16;
hence
( F is_filter-coarser_than filter_image (f,(Tails_Filter L)) iff B is_coarser_than f .: (# (Tails L)) )
by Th11; verum