reconsider cB3 = cB1 as filter_base of X1 by CARDFIL2:29;

reconsider cB4 = cB2 as filter_base of X2 by CARDFIL2:29;

reconsider cF1F2 = <.cF1,cF2.) as Filter of [:X1,X2:] ;

consider cB5 being filter_base of X1, cB6 being filter_base of X2 such that

A1: <.cB5.) = cF1 and

A2: <.cB6.) = cF2 and

A3: cF1F2 = <.[:cB5,cB6:].) by Def1;

A4: ( <.cB3.) = cF1 & <.cB4.) = cF2 ) by Th23;

[:cB3,cB4:] c= <.[:cB3,cB4:].) by CARDFIL2:18;

then reconsider cB3B4 = [:cB3,cB4:] as non empty Subset of cF1F2 by A4, A1, A2, A3, Th22;

cB3B4 is filter_basis_{1} being basis of <.cF1,cF2.) ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st

( cB1 = cB3 & cB2 = cB4 & b_{1} = [:cB3,cB4:] )
; :: thesis: verum

reconsider cB4 = cB2 as filter_base of X2 by CARDFIL2:29;

reconsider cF1F2 = <.cF1,cF2.) as Filter of [:X1,X2:] ;

consider cB5 being filter_base of X1, cB6 being filter_base of X2 such that

A1: <.cB5.) = cF1 and

A2: <.cB6.) = cF2 and

A3: cF1F2 = <.[:cB5,cB6:].) by Def1;

A4: ( <.cB3.) = cF1 & <.cB4.) = cF2 ) by Th23;

[:cB3,cB4:] c= <.[:cB3,cB4:].) by CARDFIL2:18;

then reconsider cB3B4 = [:cB3,cB4:] as non empty Subset of cF1F2 by A4, A1, A2, A3, Th22;

cB3B4 is filter_basis

proof

hence
ex b
let f be Element of cF1F2; :: according to CARDFIL2:def 7 :: thesis: ex b_{1} being M15( bool [:X1,X2:],cF1F2,cB3B4) st b_{1} c= f

f is Element of <.[:cB3,cB4:].) by A4, A1, A2, A3, Th22;

hence ex b_{1} being M15( bool [:X1,X2:],cF1F2,cB3B4) st b_{1} c= f
by CARDFIL2:def 8; :: thesis: verum

end;f is Element of <.[:cB3,cB4:].) by A4, A1, A2, A3, Th22;

hence ex b

( cB1 = cB3 & cB2 = cB4 & b