let T be non empty TopSpace; :: thesis: for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter NAT)) 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 the carrier of T; :: thesis: for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter NAT)) 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
( x in lim_filter (s,(Frechet_Filter NAT)) 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: ( x in lim_filter (s,(Frechet_Filter NAT)) 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 )
( x in lim_filter (s,(Frechet_Filter NAT)) iff B is_coarser_than s .: base_of_frechet_filter ) by Th39;
hence ( x in lim_filter (s,(Frechet_Filter NAT)) 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 Th40; :: thesis: verum