let X1, X2 be non empty set ; :: thesis: for cA1, cB1 being filter_base of X1
for cA2, cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2 st cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) holds
<.[:cB1,cB2:].) = <.[:cA1,cA2:].)
let cA1, cB1 be filter_base of X1; :: thesis: for cA2, cB2 being filter_base of X2
for cF1 being Filter of X1
for cF2 being Filter of X2 st cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) holds
<.[:cB1,cB2:].) = <.[:cA1,cA2:].)
let cA2, cB2 be filter_base of X2; :: thesis: for cF1 being Filter of X1
for cF2 being Filter of X2 st cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) holds
<.[:cB1,cB2:].) = <.[:cA1,cA2:].)
let cF1 be Filter of X1; :: thesis: for cF2 being Filter of X2 st cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) holds
<.[:cB1,cB2:].) = <.[:cA1,cA2:].)
let cF2 be Filter of X2; :: thesis: ( cF1 = <.cB1.) & cF1 = <.cA1.) & cF2 = <.cB2.) & cF2 = <.cA2.) implies <.[:cB1,cB2:].) = <.[:cA1,cA2:].) )
assume that
A1: cF1 = <.cB1.) and
A2: cF1 = <.cA1.) and
A3: cF2 = <.cB2.) and
A4: cF2 = <.cA2.) ; :: thesis: <.[:cB1,cB2:].) = <.[:cA1,cA2:].)
A5: cB1,cA1 are_equivalent_generators by A1, A2, CARDFIL2:26;
A6: cB2,cA2 are_equivalent_generators by A3, A4, CARDFIL2:26;

now :: thesis: ( ( for B being Element of [:cB1,cB2:] ex A being Element of [:cA1,cA2:] st A c= B ) & ( for A being Element of [:cA1,cA2:] ex B being Element of [:cB1,cB2:] st B c= A ) )

hereby :: thesis: for A being Element of [:cA1,cA2:] ex B being Element of [:cB1,cB2:] st B c= A

let B be Element of [:cB1,cB2:]; :: thesis: ex A being Element of [:cA1,cA2:] st A c= B
B in [:cB1,cB2:] ;
then consider B1 being Element of cB1, B2 being Element of cB2 such that
A7: B = [:B1,B2:] ;
consider B1A1 being Element of cA1 such that
A8: B1A1 c= B1 by A5;
consider B2A2 being Element of cA2 such that
A9: B2A2 c= B2 by A6;
[:B1A1,B2A2:] in [:cA1,cA2:] ;
then reconsider A = [:B1A1,B2A2:] as Element of [:cA1,cA2:] ;
( [:B1A1,B2A2:] c= [:B1,B2A2:] & [:B1,B2A2:] c= [:B1,B2:] ) by A8, A9, ZFMISC_1:95;
then A c= B by A7;
hence ex A being Element of [:cA1,cA2:] st A c= B ; :: thesis: verum

end;

hereby :: thesis: verum

let A be Element of [:cA1,cA2:]; :: thesis: ex B being Element of [:cB1,cB2:] st B c= A
A in [:cA1,cA2:] ;
then consider A1 being Element of cA1, A2 being Element of cA2 such that
A10: A = [:A1,A2:] ;
consider A1B1 being Element of cB1 such that
A11: A1B1 c= A1 by A5;
consider A2B2 being Element of cB2 such that
A12: A2B2 c= A2 by A6;
[:A1B1,A2B2:] in [:cB1,cB2:] ;
then reconsider B = [:A1B1,A2B2:] as Element of [:cB1,cB2:] ;
( [:A1B1,A2B2:] c= [:A1,A2B2:] & [:A1,A2B2:] c= [:A1,A2:] ) by A11, A12, ZFMISC_1:95;
then B c= A by A10;
hence ex B being Element of [:cB1,cB2:] st B c= A ; :: thesis: verum

end;

end;

then [:cB1,cB2:],[:cA1,cA2:] are_equivalent_generators ;
hence <.[:cB1,cB2:].) = <.[:cA1,cA2:].) by CARDFIL2:20; :: thesis: verum