let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)
let X be non-empty n -element FinSequence; :: thesis: for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)
let S be ClassicalSemiringFamily of X; :: thesis: MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)
reconsider S1 = S as cap-closed-yielding SemiringFamily of X by Thm38;
SemiringProduct S1 is cap-closed cap-finite-partition-closed diff-finite-partition-closed with_empty_element Subset-Family of (product X) by Thm32;
hence MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X) by SRINGS_3:10; :: thesis: verum