:: deftheorem Def1 defines <. CARDFIL4:def 2 :
for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for b₅ being Filter of [:X1,X2:] holds
( b₅ = <.cF1,cF2.) iff ex cB1 being filter_base of X1 ex cB2 being filter_base of X2 st
( <.cB1.) = cF1 & <.cB2.) = cF2 & b₅ = <.[:cB1,cB2:].) ) );