let X1, X2 be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: { [: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:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } or x in bool [:X1,X2:] )
assume x in { [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } ; :: thesis: x in bool [:X1,X2:]
then consider f1 being Element of F1, f2 being Element of F2 such that
A1: x = [:f1,f2:] ;
thus x in bool [:X1,X2:] by A1; :: thesis: verum

end;

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; :: thesis: verum