theorem :: MEASUR14:43

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