let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T holds lim_filter (s,(Frechet_Filter [:NAT,NAT:])) c= lim_filter (s,<.all-square-uparrow.))
let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: lim_filter (s,(Frechet_Filter [:NAT,NAT:])) c= lim_filter (s,<.all-square-uparrow.))
<.all-square-uparrow.) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by Th34, CARDFIL2:19, Th35;
hence lim_filter (s,(Frechet_Filter [:NAT,NAT:])) c= lim_filter (s,<.all-square-uparrow.)) by Th37, Th39, Th40; :: thesis: verum