:: deftheorem defines measurable_rectangles MEASUR10:def 5 :
for X1, X2 being set
for S1 being Field_Subset of X1
for S2 being Field_Subset of X2 holds measurable_rectangles (S1,S2) = { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;