theorem Th42: :: MEASUR14:42

( Prod_Field (L-Field 2) = sigma (measurable_rectangles (L-Field,L-Field)) & measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) & { [:A,B:] where A, B is Element of Borel_Sets : verum } c= measurable_rectangles (L-Field,L-Field) & { [:I,J:] where I, J is Subset of REAL : ( I is Interval & J is Interval ) } c= { [:A,B:] where A, B is Element of Borel_Sets : verum } )