let n be non zero Nat; :: thesis: MeasurableRectangle (ProductLeftOpenIntervals n) = Product (n,the_set_of_all_left_open_real_bounded_intervals)
thus MeasurableRectangle (ProductLeftOpenIntervals n) c= Product (n,the_set_of_all_left_open_real_bounded_intervals) :: according to XBOOLE_0:def 10 :: thesis: Product (n,the_set_of_all_left_open_real_bounded_intervals) c= MeasurableRectangle (ProductLeftOpenIntervals n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MeasurableRectangle (ProductLeftOpenIntervals n) or x in Product (n,the_set_of_all_left_open_real_bounded_intervals) )
assume x in MeasurableRectangle (ProductLeftOpenIntervals n) ; :: thesis: x in Product (n,the_set_of_all_left_open_real_bounded_intervals)
then consider y being Subset of (REAL n), a, b being Element of REAL n such that
A1: x = y and
A2: for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) ) ) by Th32;

now :: thesis: for t being Element of REAL n holds
( ( t in y implies for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) & ( ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) implies t in y ) )

let t be Element of REAL n; :: thesis: ( ( t in y implies for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) & ( ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) implies t in y ) )

hereby :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) implies t in y )

assume A3: t in y ; :: thesis: for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).]

hereby :: thesis: verum

let i be Nat; :: thesis: ( i in Seg n implies t . i in ].(a . i),(b . i).] )
assume A4: i in Seg n ; :: thesis: t . i in ].(a . i),(b . i).]
consider t0 being Element of REAL n such that
A5: t = t0 and
A6: for i being Nat st i in Seg n holds
t0 . i in ].(a . i),(b . i).] by A3, A2;
thus t . i in ].(a . i),(b . i).] by A6, A4, A5; :: thesis: verum

end;

end;

assume for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ; :: thesis: t in y
hence t in y by A2; :: thesis: verum

end;

then y is Element of Product (n,the_set_of_all_left_open_real_bounded_intervals) by Th44;
hence x in Product (n,the_set_of_all_left_open_real_bounded_intervals) by A1; :: thesis: verum

end;

thus Product (n,the_set_of_all_left_open_real_bounded_intervals) c= MeasurableRectangle (ProductLeftOpenIntervals n) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Product (n,the_set_of_all_left_open_real_bounded_intervals) or x in MeasurableRectangle (ProductLeftOpenIntervals n) )
assume x in Product (n,the_set_of_all_left_open_real_bounded_intervals) ; :: thesis: x in MeasurableRectangle (ProductLeftOpenIntervals n)
then consider g being Function such that
A7: x = product g and
A8: g in product ((Seg n) --> the_set_of_all_left_open_real_bounded_intervals) by Def2;
thus x in MeasurableRectangle (ProductLeftOpenIntervals n) by A7, A8, SRINGS_4:def 4; :: thesis: verum

end;