let X1, X2 be 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:]
let F1 be 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:]
let F2 be Filter of X2; { [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } is non empty Subset-Family of [:X1,X2:]
set F1xF2 = { [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } ;
A0:
[: the Element of F1, the Element of F2:] in { [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum }
;
{ [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } c= bool [:X1,X2:]
hence
{ [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } is non empty Subset-Family of [:X1,X2:]
by A0; verum