set cB12 = { [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } ;
reconsider cB1a = cB1 as non empty Subset-Family of X1 ;
reconsider cB2a = cB2 as non empty Subset-Family of X2 ;
set cB12a = { [:B1,B2:] where B1 is Element of cB1a, B2 is Element of cB2a : verum } ;
{ [:B1,B2:] where B1 is Element of cB1a, B2 is Element of cB2a : verum } = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in cB1a & x2 in cB2a & s = [:x1,x2:] ) } by SRINGS_2:2;
then reconsider cB12 = { [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } as Subset-Family of [:X1,X2:] by Th3;
now :: thesis: ( not cB12 is empty & cB12 is with_non-empty_elements & cB12 is quasi_basis )
thus A1: not cB12 is empty :: thesis: ( cB12 is with_non-empty_elements & cB12 is quasi_basis )
proof
set B1 = the Element of cB1a;
set B2 = the Element of cB2a;
[: the Element of cB1a, the Element of cB2a:] in cB12 ;
hence not cB12 is empty ; :: thesis: verum
end;
thus cB12 is with_non-empty_elements :: thesis: cB12 is quasi_basis
proof
assume not cB12 is with_non-empty_elements ; :: thesis: contradiction
then {} in cB12 by SETFAM_1:def 8;
then ex B1 being Element of cB1a ex B2 being Element of cB2a st {} = [:B1,B2:] ;
hence contradiction ; :: thesis: verum
end;
thus cB12 is quasi_basis :: thesis: verum
proof
hereby :: according to CARDFIL2:def 11 :: thesis: verum
let b1, b2 be Element of cB12; :: thesis: ex b being Element of cB12 st b c= b1 /\ b2
b1 in cB12 by A1;
then consider b11 being Element of cB1, b12 being Element of cB2 such that
A2: b1 = [:b11,b12:] ;
b2 in cB12 by A1;
then consider b21 being Element of cB1, b22 being Element of cB2 such that
A3: b2 = [:b21,b22:] ;
cB1 is quasi_basis ;
then consider a1 being Element of cB1 such that
A4: a1 c= b11 /\ b21 ;
cB2 is quasi_basis ;
then consider a2 being Element of cB2 such that
A5: a2 c= b12 /\ b22 ;
[:a1,a2:] in cB12 ;
then reconsider b = [:a1,a2:] as Element of cB12 ;
( [:a1,a2:] c= [:(b11 /\ b21),a2:] & [:(b11 /\ b21),a2:] c= [:(b11 /\ b21),(b12 /\ b22):] ) by A4, A5, ZFMISC_1:95;
then [:a1,a2:] c= [:(b11 /\ b21),(b12 /\ b22):] ;
then b c= b1 /\ b2 by A2, A3, ZFMISC_1:100;
hence ex b being Element of cB12 st b c= b1 /\ b2 ; :: thesis: verum
end;
end;
end;
hence { [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } is filter_base of [:X1,X2:] ; :: thesis: verum