let X1, X2 be non empty set ; 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; 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; 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; 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; ( 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.)
; <.[: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 ( ( 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 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:];
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
;
verum
end; hereby verum
let A be
Element of
[:cA1,cA2:];
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
;
verum
end;
then
[:cB1,cB2:],[:cA1,cA2:] are_equivalent_generators
;
hence
<.[:cB1,cB2:].) = <.[:cA1,cA2:].)
by CARDFIL2:20; verum