theorem :: CARDFIL2:2

for X1, X2 being non empty set
for F1 being Filter of X1
for F2 being Filter of X2 holds { [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } is non empty Subset-Family of [:X1,X2:]