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

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

let z be object ; :: thesis: ( z in { [:A,B:] where A, B is Element of Borel_Sets : verum } implies z in measurable_rectangles (L-Field,L-Field) )
assume z in { [:A,B:] where A, B is Element of Borel_Sets : verum } ; :: thesis: z in measurable_rectangles (L-Field,L-Field)
then consider A, B being Element of Borel_Sets such that
A7: z = [:A,B:] ;
( A in L-Field & B in L-Field ) by MEASUR12:75;
hence z in measurable_rectangles (L-Field,L-Field) by A7; :: thesis: verum

end;

hence { [:A,B:] where A, B is Element of Borel_Sets : verum } c= measurable_rectangles (L-Field,L-Field) ; :: thesis: { [: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 }
set IJ = { [:I,J:] where I, J is Subset of REAL : ( I is Interval & J is Interval ) } ;

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

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

end;

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