theorem Th45: :: CARDFIL4:54

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