for X being non empty set
for s being sequence of X
for B being filter_base of X holds
( B is_coarser_than s .: base_of_frechet_filter iff for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) by Th20;