:: deftheorem Def2 defines [: CARDFIL4:def 3 :
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for cB1 being basis of cF1
for cB2 being basis of cF2
for b₇ being basis of <.cF1,cF2.) holds
( b₇ = [:cB1,cB2:] iff ex cB3 being filter_base of X1 ex cB4 being filter_base of X2 st
( cB1 = cB3 & cB2 = cB4 & b₇ = [:cB3,cB4:] ) );