consider cB being basis of such that
A1: cB = base_of_frechet_filter and
[:cB,cB:] is basis of by Th33;
<.(# [:cB,cB:]).] =
proof
set cF1 = <.(# [:cB,cB:]).];
set cF2 = ;
now :: thesis: for x being object st x in <.(# [:cB,cB:]).] holds
x in
let x be object ; :: thesis: ( x in <.(# [:cB,cB:]).] implies x in )
assume A2: x in <.(# [:cB,cB:]).] ; :: thesis:
then reconsider y = x as Subset of ;
consider b being Element of # [:cB,cB:] such that
A3: b c= y by ;
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 by A1, A4, A5, A7;
hence x in by ; :: thesis: verum
end;
then A8: <.(# [:cB,cB:]).] c= ;
now :: thesis: for x being object st x in holds
x in <.(# [:cB,cB:]).]
let x be object ; :: thesis: ( x in implies x in <.(# [:cB,cB:]).] )
assume A9: x in ; :: thesis: x in <.(# [:cB,cB:]).]
then reconsider y = x as Subset of ;
consider b being Element of such that
A10: b c= y by ;
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 ; :: thesis: verum
end;
then <..) c= <.(# [:cB,cB:]).] ;
hence <.(# [:cB,cB:]).] = by A8; :: thesis: verum
end;
hence <..) = by CARDFIL2:21; :: thesis: verum