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
proof
let f be
Element of
cF1F2;
CARDFIL2:def 7 ex b1 being M15( bool [:X1,X2:],cF1F2,cB3B4) st b1 c= f
f is
Element of
<.[:cB3,cB4:].)
by A4, A1, A2, A3, Th22;
hence
ex
b1 being
M15(
bool [:X1,X2:],
cF1F2,
cB3B4) st
b1 c= f
by CARDFIL2:def 8;
verum
end;
hence
ex b1 being basis of <.cF1,cF2.) ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st
( cB1 = cB3 & cB2 = cB4 & b1 = [:cB3,cB4:] )
; verum