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