for T being non empty TopSpace
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.))