set X = (Seg 3) --> REAL;
A1: len (SubFin (((Seg 3) --> REAL),1)) = 1 by CARD_1:def 7;
A2: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) ;
A3: ( 1 in Seg 2 & 2 in Seg 2 ) ;
A4: 1 in Seg 1 ;
consider S2 being SigmaField of (CarProduct (SubFin (((Seg 3) --> REAL),2))) such that
A5: ( S2 = (ProdSigmaFldFinSeq (L-Field 3)) . 2 & (ProdSigmaFldFinSeq (L-Field 3)) . (2 + 1) = sigma (measurable_rectangles (S2,(ElmFin ((L-Field 3),(2 + 1))))) ) by MEASUR13:def 11;
consider S1 being SigmaField of (CarProduct (SubFin (((Seg 3) --> REAL),1))) such that
A6: ( S1 = (ProdSigmaFldFinSeq (L-Field 3)) . 1 & (ProdSigmaFldFinSeq (L-Field 3)) . (1 + 1) = sigma (measurable_rectangles (S1,(ElmFin ((L-Field 3),(1 + 1))))) ) by MEASUR13:def 11;
SubFin (((Seg 3) --> REAL),1) = ((Seg 3) --> REAL) | 1 by MEASUR13:def 5;
then (SubFin (((Seg 3) --> REAL),1)) . 1 = ((Seg 3) --> REAL) . 1 by A4, FUNCT_1:49;
then SubFin (((Seg 3) --> REAL),1) = <*REAL*> by A1, A2, FUNCOP_1:7, FINSEQ_1:40;
then a7: CarProduct (SubFin (((Seg 3) --> REAL),1)) = <*REAL*> . 1 by MEASUR13:def 3;
SubFin (((Seg 3) --> REAL),2) = ((Seg 3) --> REAL) | 2 by MEASUR13:def 5;
then ( (SubFin (((Seg 3) --> REAL),2)) . 1 = ((Seg 3) --> REAL) . 1 & (SubFin (((Seg 3) --> REAL),2)) . 2 = ((Seg 3) --> REAL) . 2 ) by A3, FUNCT_1:49;
then A8: ( (SubFin (((Seg 3) --> REAL),2)) . 1 = REAL & (SubFin (((Seg 3) --> REAL),2)) . 2 = REAL ) by A2, FUNCOP_1:7;
then (ProdFinSeq (SubFin (((Seg 3) --> REAL),2))) . 1 = REAL by MEASUR13:def 3;
then A9: (ProdFinSeq (SubFin (((Seg 3) --> REAL),2))) . (1 + 1) = [:REAL,REAL:] by A8, MEASUR13:def 3;
(ProdSigmaFldFinSeq (L-Field 3)) . 1 = (L-Field 3) . 1 by MEASUR13:def 11;
then A10: S1 = L-Field by A6, A2, FUNCOP_1:7;
ElmFin (((Seg 3) --> REAL),2) = ((Seg 3) --> REAL) . 2 by MEASUR13:def 1;
then A11: ElmFin (((Seg 3) --> REAL),2) = REAL by A2, FUNCOP_1:7;
ElmFin ((L-Field 3),2) = (L-Field 3) . 2 by MEASUR13:def 7;
then A12: ElmFin ((L-Field 3),2) = L-Field by A2, FUNCOP_1:7;
ElmFin (((Seg 3) --> REAL),3) = ((Seg 3) --> REAL) . 3 by MEASUR13:def 1;
then A13: ElmFin (((Seg 3) --> REAL),3) = REAL by A2, FUNCOP_1:7;
ElmFin ((L-Field 3),3) = (L-Field 3) . 3 by MEASUR13:def 7;
hence Prod_Field (L-Field 3) = sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by A9, A11, A12, a7, A6, A10, A5, A13, A2, FUNCOP_1:7; :: thesis: ( 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 } )
thus 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; :: thesis: ( { [: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 } )
set XYZ = { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } ;

now :: thesis: for z being object st z in { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } holds
z in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)

let z be object ; :: thesis: ( z in { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } implies z in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) )
assume z in { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } ; :: thesis: z in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)
then consider A, B, C being Element of Borel_Sets such that
A14: z = [:A,B,C:] ;
A15: ( A in L-Field & B in L-Field & C in L-Field ) by MEASUR12:75;
then A16: [:A,B:] 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;
then [:[:A,B:],C:] in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) by A15, A16;
hence z in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) by A14, ZFMISC_1:def 3; :: thesis: verum

end;

hence { [: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) ; :: thesis: { [: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 }
set IJK = { [:I,J,K:] where I, J, K is Subset of REAL : ( I is Interval & J is Interval & K is Interval ) } ;

now :: thesis: for z being object st z in { [:I,J,K:] where I, J, K is Subset of REAL : ( I is Interval & J is Interval & K is Interval ) } holds
z in { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum }

let z be object ; :: thesis: ( z in { [:I,J,K:] where I, J, K is Subset of REAL : ( I is Interval & J is Interval & K is Interval ) } implies z in { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } )
assume z in { [:I,J,K:] where I, J, K is Subset of REAL : ( I is Interval & J is Interval & K is Interval ) } ; :: thesis: z in { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum }
then consider I, J, K being Subset of REAL such that
A17: ( z = [:I,J,K:] & I is Interval & J is Interval & K is Interval ) ;
( I in Borel_Sets & J in Borel_Sets & K in Borel_Sets ) by A17, MEASUR10:5;
hence z in { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } by A17; :: thesis: verum

end;

hence { [: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 } ; :: thesis: verum