let T be non empty TopSpace; :: thesis: for s being sequence of ([#] T)
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem 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 )
let s be sequence of ([#] T); :: thesis: for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem 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 )
let x be Point of T; :: thesis: for B being basis of (BOOL2F (NeighborhoodSystem 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 )
let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( 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 )
reconsider B = B as filter_base of ([#] T) by Th09;
( 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;
hence ( 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 ) ; :: thesis: verum