let X be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( [#] 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 ; :: thesis: ( 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; :: thesis: verum