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;

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

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 ) )end;

then
[:cB1,cB2:],[:cA1,cA2:] are_equivalent_generators
;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;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

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;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

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