theorem Th44: :: CARDFIL4:53

for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M }