consider cB being basis of (Frechet_Filter NAT) such that
A1: cB = base_of_frechet_filter and
[:cB,cB:] is basis of <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by Th33;
<.(# [:cB,cB:]).] = <.[:base_of_frechet_filter,base_of_frechet_filter:].)

proof

set cF1 = <.(# [:cB,cB:]).];
set cF2 = <.[:base_of_frechet_filter,base_of_frechet_filter:].);

now :: thesis: for x being object st x in <.(# [:cB,cB:]).] holds
x in <.[:base_of_frechet_filter,base_of_frechet_filter:].)

let x be object ; :: thesis: ( x in <.(# [:cB,cB:]).] implies x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) )
assume A2: x in <.(# [:cB,cB:]).] ; :: thesis: x in <.[:base_of_frechet_filter,base_of_frechet_filter:].)
then reconsider y = x as Subset of [:NAT,NAT:] ;
consider b being Element of # [:cB,cB:] such that
A3: b c= y by A2, CARDFIL2:def 8;
consider cB3, cB4 being filter_base of NAT such that
A4: cB = cB3 and
A5: cB = cB4 and
A6: [:cB,cB:] = [:cB3,cB4:] by Def2;
b in { [:B1,B2:] where B1 is Element of cB3, B2 is Element of cB4 : verum } by A6;
then consider B1 being Element of cB3, B2 being Element of cB4 such that
A7: b = [:B1,B2:] ;
b in [:base_of_frechet_filter,base_of_frechet_filter:] by A1, A4, A5, A7;
hence x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) by A3, CARDFIL2:def 8; :: thesis: verum

end;

then A8: <.(# [:cB,cB:]).] c= <.[:base_of_frechet_filter,base_of_frechet_filter:].) ;

now :: thesis: for x being object st x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) holds
x in <.(# [:cB,cB:]).]

let x be object ; :: thesis: ( x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) implies x in <.(# [:cB,cB:]).] )
assume A9: x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) ; :: thesis: x in <.(# [:cB,cB:]).]
then reconsider y = x as Subset of [:NAT,NAT:] ;
consider b being Element of [:base_of_frechet_filter,base_of_frechet_filter:] such that
A10: b c= y by A9, CARDFIL2:def 8;
ex cB3, cB4 being filter_base of NAT st
( cB = cB3 & cB = cB4 & [:cB,cB:] = [:cB3,cB4:] ) by Def2;
hence x in <.(# [:cB,cB:]).] by A1, A10, CARDFIL2:def 8; :: thesis: verum

end;

then <.[:base_of_frechet_filter,base_of_frechet_filter:].) c= <.(# [:cB,cB:]).] ;
hence <.(# [:cB,cB:]).] = <.[:base_of_frechet_filter,base_of_frechet_filter:].) by A8; :: thesis: verum

end;

hence <.[:base_of_frechet_filter,base_of_frechet_filter:].) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by CARDFIL2:21; :: thesis: verum