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;

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 )

hence
{ [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } is filter_base of [:X1,X2:]
; :: thesis: verumthus A1:
not cB12 is empty
:: thesis: ( cB12 is with_non-empty_elements & cB12 is quasi_basis )

end;proof

thus
cB12 is with_non-empty_elements
:: thesis: cB12 is quasi_basis
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;set B2 = the Element of cB2a;

[: the Element of cB1a, the Element of cB2a:] in cB12 ;

hence not cB12 is empty ; :: thesis: verum

proof

thus
cB12 is quasi_basis
:: thesis: verum
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;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

proof
end;

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