for X1, X2 being set
for F1 being Field_Subset of X1
for F2 being Field_Subset of X2 holds { [:A,B:] where A is Element of F1, B is Element of F2 : verum } is semialgebra_of_sets of [:X1,X2:]