now :: thesis: for x being object st x in Frechet_Filter [:NAT,NAT:] holds
x in <.(Frechet_Filter NAT),(Frechet_Filter NAT).)

let x be object ; :: thesis: ( x in Frechet_Filter [:NAT,NAT:] implies x in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) )
assume A1: x in Frechet_Filter [:NAT,NAT:] ; :: thesis: x in <.(Frechet_Filter NAT),(Frechet_Filter NAT).)
x in { ([:NAT,NAT:] \ A) where A is finite Subset of [:NAT,NAT:] : verum } by A1, CARDFIL2:51;
then consider A being finite Subset of [:NAT,NAT:] such that
A2: x = [:NAT,NAT:] \ A ;
reconsider y = x as Subset of [:NAT,NAT:] by A2;
consider m, n being Nat such that
A3: A c= [:(Segm m),(Segm n):] by Th16;
A4: [:NAT,NAT:] \ [:(Segm m),(Segm n):] c= y by A2, A3, XBOOLE_1:34;
[:(NAT \ (Segm m)),(NAT \ (Segm n)):] c= [:NAT,NAT:] \ [:(Segm m),(Segm n):] by Th10;
then A5: [:(NAT \ (Segm m)),(NAT \ (Segm n)):] c= y by A4;
( NAT \ (Segm m) is Element of base_of_frechet_filter & NAT \ (Segm n) is Element of base_of_frechet_filter ) by Th21;
then [:(NAT \ (Segm m)),(NAT \ (Segm n)):] in [:base_of_frechet_filter,base_of_frechet_filter:] ;
hence x in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by Th35, A5, CARDFIL2:def 8; :: thesis: verum

end;

then Frechet_Filter [:NAT,NAT:] c= <.(Frechet_Filter NAT),(Frechet_Filter NAT).) ;
hence <.(Frechet_Filter NAT),(Frechet_Filter NAT).) is_filter-finer_than Frechet_Filter [:NAT,NAT:] ; :: thesis: verum