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 )

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

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
ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A
; :: thesis: 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;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

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