let T be 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 )
let s be 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 )
let M be Subset of the carrier of T; ( s " M in Frechet_Filter [:NAT,NAT:] iff ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A )
assume
ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A
; s " M in Frechet_Filter [:NAT,NAT:]
then
s " M in { ([:NAT,NAT:] \ A) where A is finite Subset of [:NAT,NAT:] : verum }
;
hence
s " M in Frechet_Filter [:NAT,NAT:]
by CARDFIL2:51; verum