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