let I, J be Interval; :: thesis: ( [:I,J:] is Subset of [:RNS_Real,RNS_Real:] & [:I,J:] in sigma (measurable_rectangles (L-Field,L-Field)) )
( I in L-Field & J in L-Field ) by MEASUR10:5, MEASUR12:75;
then A1: [:I,J:] in measurable_rectangles (L-Field,L-Field) ;
measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:def 9;
hence ( [:I,J:] is Subset of [:RNS_Real,RNS_Real:] & [:I,J:] in sigma (measurable_rectangles (L-Field,L-Field)) ) by A1; :: thesis: verum