theorem Th41: :: CARDFIL4:50

for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T
for M being Subset of the carrier of T holds
( s " M in Frechet_Filter [:NAT,NAT:] iff ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A )