:: deftheorem defines [: CARDFIL4:def 1 :
for X1, X2 being non empty set
for cB1 being filter_base of X1
for cB2 being filter_base of X2 holds [:cB1,cB2:] = { [:B1,B2:] where B1 is Element of cB1, B2 is Element of cB2 : verum } ;