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:].)

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

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

set cF2 = <.[:base_of_frechet_filter,base_of_frechet_filter:].);

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

end;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:].)

then A8:
<.(# [:cB,cB:]).] c= <.[:base_of_frechet_filter,base_of_frechet_filter:].)
;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;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

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

x in <.(# [:cB,cB:]).]

then
<.[:base_of_frechet_filter,base_of_frechet_filter:].) c= <.(# [:cB,cB:]).]
;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;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

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