let A be Subset of [:RNS_Real,RNS_Real,RNS_Real:]; :: thesis: ( A is open implies A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) )
assume A1: A is open ; :: thesis: A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
set LF2 = sigma (measurable_rectangles (L-Field,L-Field));
set LF3 = sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field));
per cases ( A = {} or A <> {} ) ;
suppose A = {} ; :: thesis: A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
hence A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by PROB_1:4; :: thesis: verum
end;
suppose A2: A <> {} ; :: thesis: A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
per cases ( ex a, b, c being Real st
( [a,b,c] in A & ( for Rx being real-membered set holds
( Rx is empty or not Rx is bounded_above or not Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ) ) ) or for a, b, c being Real st [a,b,c] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ) ) ;
suppose ex a, b, c being Real st
( [a,b,c] in A & ( for Rx being real-membered set holds
( Rx is empty or not Rx is bounded_above or not Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ) ) ) ; :: thesis: A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
then consider a, b, c being Real such that
A3: ( [a,b,c] in A & ( for Rx being real-membered set holds
( Rx is empty or not Rx is bounded_above or not Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ) ) ) ;
set Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ;
now :: thesis: for z being object st z in { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } holds
z is real
let z be object ; :: thesis: ( z in { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } implies z is real )
assume z in { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ; :: thesis: z is real
then ex r being Real st
( z = r & 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) ;
hence z is real ; :: thesis: verum
end;
then reconsider Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } as real-membered set by MEMBERED:def 3;
reconsider a1 = a, b1 = b, c1 = c as Point of RNS_Real by XREAL_0:def 1;
reconsider x = [a1,b1,c1] as Point of [:RNS_Real,RNS_Real,RNS_Real:] ;
consider r0 being Real such that
A4: ( r0 > 0 & Ball (x,r0) c= A ) by A1, A3, NDIFF_8:20;
consider s, aa, bb, cc being Real such that
A5: ( 0 < s & s < r0 & x = [aa,bb,cc] & [:].(aa - s),(aa + s).[,].(bb - s),(bb + s).[,].(cc - s),(cc + s).[:] c= Ball (x,r0) ) by A4, Th5;
A6: [:].(aa - s),(aa + s).[,].(bb - s),(bb + s).[,].(cc - s),(cc + s).[:] c= A by A5, A4;
( a = aa & b = bb & c = cc ) by A5, XTUPLE_0:3;
then s in Rx by A5, A6;
then A7: not Rx is bounded_above by A3;
now :: thesis: for u being object st u in [:REAL,REAL,REAL:] holds
u in A
let u be object ; :: thesis: ( u in [:REAL,REAL,REAL:] implies u in A )
assume u in [:REAL,REAL,REAL:] ; :: thesis: u in A
then consider xy1, z1 being object such that
A8: ( xy1 in [:REAL,REAL:] & z1 in REAL & u = [xy1,z1] ) by ZFMISC_1:def 2;
consider x1, y1 being object such that
A9: ( x1 in REAL & y1 in REAL & xy1 = [x1,y1] ) by A8, ZFMISC_1:def 2;
reconsider x1 = x1, y1 = y1, z1 = z1 as Real by A8, A9;
consider r1 being Real such that
A10: ( 0 < r1 & x1 in ].(a - r1),(a + r1).[ ) by Lm1;
consider r2 being Real such that
A11: ( 0 < r2 & y1 in ].(b - r2),(b + r2).[ ) by Lm1;
consider r3 being Real such that
A12: ( 0 < r3 & z1 in ].(c - r3),(c + r3).[ ) by Lm1;
set r = max ((max (r1,r2)),r3);
A13: ( r1 <= max (r1,r2) & r2 <= max (r1,r2) ) by XXREAL_0:25;
( max (r1,r2) <= max ((max (r1,r2)),r3) & r3 <= max ((max (r1,r2)),r3) ) by XXREAL_0:25;
then A14: ( ].(a - r1),(a + r1).[ c= ].(a - (max ((max (r1,r2)),r3))),(a + (max ((max (r1,r2)),r3))).[ & ].(b - r2),(b + r2).[ c= ].(b - (max ((max (r1,r2)),r3))),(b + (max ((max (r1,r2)),r3))).[ & ].(c - r3),(c + r3).[ c= ].(c - (max ((max (r1,r2)),r3))),(c + (max ((max (r1,r2)),r3))).[ ) by Lm2, XXREAL_0:2, A13;
then [x1,y1] in [:].(a - (max ((max (r1,r2)),r3))),(a + (max ((max (r1,r2)),r3))).[,].(b - (max ((max (r1,r2)),r3))),(b + (max ((max (r1,r2)),r3))).[:] by A10, A11, ZFMISC_1:87;
then A15: u in [:].(a - (max ((max (r1,r2)),r3))),(a + (max ((max (r1,r2)),r3))).[,].(b - (max ((max (r1,r2)),r3))),(b + (max ((max (r1,r2)),r3))).[,].(c - (max ((max (r1,r2)),r3))),(c + (max ((max (r1,r2)),r3))).[:] by A8, A9, A12, A14, ZFMISC_1:87;
max ((max (r1,r2)),r3) is not UpperBound of Rx by A7, XXREAL_2:def 10;
then consider s being ExtReal such that
A16: ( s in Rx & max ((max (r1,r2)),r3) < s ) by XXREAL_2:def 1;
reconsider s = s as Real by A16;
A17: ex s0 being Real st
( s = s0 & 0 < s0 & [:].(a - s0),(a + s0).[,].(b - s0),(b + s0).[,].(c - s0),(c + s0).[:] c= A ) by A16;
A18: ( ].(a - (max ((max (r1,r2)),r3))),(a + (max ((max (r1,r2)),r3))).[ c= ].(a - s),(a + s).[ & ].(b - (max ((max (r1,r2)),r3))),(b + (max ((max (r1,r2)),r3))).[ c= ].(b - s),(b + s).[ & ].(c - (max ((max (r1,r2)),r3))),(c + (max ((max (r1,r2)),r3))).[ c= ].(c - s),(c + s).[ ) by A16, Lm2;
then [:].(a - (max ((max (r1,r2)),r3))),(a + (max ((max (r1,r2)),r3))).[,].(b - (max ((max (r1,r2)),r3))),(b + (max ((max (r1,r2)),r3))).[:] c= [:].(a - s),(a + s).[,].(b - s),(b + s).[:] by ZFMISC_1:96;
then [:[:].(a - (max ((max (r1,r2)),r3))),(a + (max ((max (r1,r2)),r3))).[,].(b - (max ((max (r1,r2)),r3))),(b + (max ((max (r1,r2)),r3))).[:],].(c - (max ((max (r1,r2)),r3))),(c + (max ((max (r1,r2)),r3))).[:] c= [:].(a - s),(a + s).[,].(b - s),(b + s).[,].(c - s),(c + s).[:] by ZFMISC_1:96, A18;
hence u in A by A15, A17; :: thesis: verum
end;
then [:REAL,REAL,REAL:] c= A ;
then A19: A = [:REAL,REAL,REAL:] ;
A20: ( REAL in L-Field & REAL in L-Field & REAL in L-Field ) by PROB_1:5;
then A21: [:REAL,REAL:] 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 A22: [:REAL,REAL,REAL:] in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) by A20, A21;
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 A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by A19, A22; :: thesis: verum
end;
suppose for a, b, c being Real st [a,b,c] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ) ; :: thesis: A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
then consider F being Function of A,REAL such that
A23: for a, b, c being Real st [a,b,c] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } & F . [a,b,c] = (upper_bound Rx) / 2 ) by Th6;
A /\ [:RAT,RAT,RAT:] <> {}
proof
consider v being object such that
A24: v in A by A2, XBOOLE_0:def 1;
reconsider u = v as Point of [:RNS_Real,RNS_Real,RNS_Real:] by A24;
consider e0 being Real such that
A25: ( e0 > 0 & Ball (u,e0) c= A ) by A24, A1, NDIFF_8:20;
set e1 = e0 / 2;
A26: ( 0 < e0 / 2 & e0 / 2 < e0 ) by A25, XREAL_1:215, XREAL_1:216;
set e = (e0 / 2) / 3;
A27: ( 0 < (e0 / 2) / 3 & (e0 / 2) / 3 < e0 / 2 ) by A26, XREAL_1:221, XREAL_1:222;
then A28: (e0 / 2) / 3 < e0 by A26, XXREAL_0:2;
consider x1, y1, z1 being Point of RNS_Real such that
A29: u = [x1,y1,z1] by PRVECT_4:9;
reconsider xx1 = x1, yy1 = y1, zz1 = z1 as Real ;
A30: xx1 - (((e0 / 2) / 3) / 3) < xx1 by A27, XREAL_1:222, XREAL_1:44;
xx1 < xx1 + (((e0 / 2) / 3) / 3) by A27, XREAL_1:222, XREAL_1:29;
then xx1 - (((e0 / 2) / 3) / 3) < xx1 + (((e0 / 2) / 3) / 3) by A30, XXREAL_0:2;
then consider qx1 being Rational such that
A31: ( xx1 - (((e0 / 2) / 3) / 3) < qx1 & qx1 < xx1 + (((e0 / 2) / 3) / 3) ) by RAT_1:7;
qx1 in ].(xx1 - (((e0 / 2) / 3) / 3)),(xx1 + (((e0 / 2) / 3) / 3)).[ by A31;
then A32: |.(qx1 - xx1).| < ((e0 / 2) / 3) / 3 by RCOMP_1:1;
A33: yy1 - (((e0 / 2) / 3) / 3) < yy1 by A27, XREAL_1:222, XREAL_1:44;
yy1 < yy1 + (((e0 / 2) / 3) / 3) by A27, XREAL_1:222, XREAL_1:29;
then yy1 - (((e0 / 2) / 3) / 3) < yy1 + (((e0 / 2) / 3) / 3) by A33, XXREAL_0:2;
then consider qy1 being Rational such that
A34: ( yy1 - (((e0 / 2) / 3) / 3) < qy1 & qy1 < yy1 + (((e0 / 2) / 3) / 3) ) by RAT_1:7;
qy1 in ].(yy1 - (((e0 / 2) / 3) / 3)),(yy1 + (((e0 / 2) / 3) / 3)).[ by A34;
then A35: |.(qy1 - yy1).| < ((e0 / 2) / 3) / 3 by RCOMP_1:1;
A36: zz1 - (((e0 / 2) / 3) / 3) < zz1 by A27, XREAL_1:222, XREAL_1:44;
zz1 < zz1 + (((e0 / 2) / 3) / 3) by A27, XREAL_1:222, XREAL_1:29;
then zz1 - (((e0 / 2) / 3) / 3) < zz1 + (((e0 / 2) / 3) / 3) by A36, XXREAL_0:2;
then consider qz1 being Rational such that
A37: ( zz1 - (((e0 / 2) / 3) / 3) < qz1 & qz1 < zz1 + (((e0 / 2) / 3) / 3) ) by RAT_1:7;
qz1 in ].(zz1 - (((e0 / 2) / 3) / 3)),(zz1 + (((e0 / 2) / 3) / 3)).[ by A37;
then A38: |.(qz1 - zz1).| < ((e0 / 2) / 3) / 3 by RCOMP_1:1;
A39: ( qx1 in RAT & qy1 in RAT & qz1 in RAT ) by RAT_1:def 2;
reconsider dx1 = qx1, dy1 = qy1, dz1 = qz1 as Point of RNS_Real by XREAL_0:def 1;
( dx1 - x1 = qx1 - xx1 & dy1 - y1 = qy1 - yy1 & dz1 - z1 = qz1 - zz1 ) by DUALSP03:4;
then A40: ( ||.(dx1 - x1).|| < ((e0 / 2) / 3) / 3 & ||.(dy1 - y1).|| < ((e0 / 2) / 3) / 3 & ||.(dz1 - z1).|| < ((e0 / 2) / 3) / 3 ) by A32, A35, A38, EUCLID:def 2;
reconsider v = [dx1,dy1,dz1] as Point of [:RNS_Real,RNS_Real,RNS_Real:] ;
A41: - v = [(- dx1),(- dy1),(- dz1)] by PRVECT_4:9;
u - v = [(x1 + (- dx1)),(y1 + (- dy1)),(z1 + (- dz1))] by A29, A41, PRVECT_4:9;
then ||.(u - v).|| <= (||.(x1 - dx1).|| + ||.(y1 - dy1).||) + ||.(z1 - dz1).|| by Th1;
then ||.(u - v).|| <= (||.(dx1 - x1).|| + ||.(y1 - dy1).||) + ||.(z1 - dz1).|| by NORMSP_1:7;
then ||.(u - v).|| <= (||.(dx1 - x1).|| + ||.(dy1 - y1).||) + ||.(z1 - dz1).|| by NORMSP_1:7;
then A42: ||.(u - v).|| <= (||.(dx1 - x1).|| + ||.(dy1 - y1).||) + ||.(dz1 - z1).|| by NORMSP_1:7;
||.(dx1 - x1).|| + ||.(dy1 - y1).|| <= (((e0 / 2) / 3) / 3) + (((e0 / 2) / 3) / 3) by A40, XREAL_1:7;
then (||.(dx1 - x1).|| + ||.(dy1 - y1).||) + ||.(dz1 - z1).|| <= ((((e0 / 2) / 3) / 3) + (((e0 / 2) / 3) / 3)) + (((e0 / 2) / 3) / 3) by A40, XREAL_1:7;
then ||.(u - v).|| <= (e0 / 2) / 3 by A42, XXREAL_0:2;
then ||.(u - v).|| < e0 by XXREAL_0:2, A28;
then A43: v in Ball (u,e0) ;
[qx1,qy1] in [:RAT,RAT:] by A39, ZFMISC_1:87;
then [qx1,qy1,qz1] in [:RAT,RAT,RAT:] by A39, ZFMISC_1:87;
hence A /\ [:RAT,RAT,RAT:] <> {} by A25, A43, XBOOLE_0:def 4; :: thesis: verum
end;
then consider p being sequence of [:REAL,REAL,REAL:] such that
A44: rng p = A /\ [:RAT,RAT,RAT:] by Lm3;
A45: for a, b, c being Real st [a,b,c] in A holds
ex r being Real st
( 0 < r & r = F . [a,b,c] & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A )
proof
let a, b, c be Real; :: thesis: ( [a,b,c] in A implies ex r being Real st
( 0 < r & r = F . [a,b,c] & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) )
assume [a,b,c] in A ; :: thesis: ex r being Real st
( 0 < r & r = F . [a,b,c] & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A )
then consider Rx being real-membered set such that
A46: ( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } & F . [a,b,c] = (upper_bound Rx) / 2 ) by A23;
take r0 = F . [a,b,c]; :: thesis: ( 0 < r0 & r0 = F . [a,b,c] & [:].(a - r0),(a + r0).[,].(b - r0),(b + r0).[,].(c - r0),(c + r0).[:] c= A )
consider r1 being Real such that
A47: r1 in Rx by A46;
A48: ex r being Real st
( r1 = r & 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) by A46, A47;
A49: r1 <= upper_bound Rx by SEQ_4:def 1, A46, A47;
then ( 0 < r0 & r0 < upper_bound Rx ) by A46, A48, XREAL_1:215, XREAL_1:216;
then consider s being Real such that
A50: ( s in Rx & (upper_bound Rx) - r0 < s ) by A46, SEQ_4:def 1;
A51: ex r being Real st
( s = r & 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) by A50, A46;
A52: ( ].(a - r0),(a + r0).[ c= ].(a - s),(a + s).[ & ].(b - r0),(b + r0).[ c= ].(b - s),(b + s).[ & ].(c - r0),(c + r0).[ c= ].(c - s),(c + s).[ ) by A50, A46, Lm2;
then [:].(a - r0),(a + r0).[,].(b - r0),(b + r0).[:] c= [:].(a - s),(a + s).[,].(b - s),(b + s).[:] by ZFMISC_1:96;
then [:[:].(a - r0),(a + r0).[,].(b - r0),(b + r0).[:],].(c - r0),(c + r0).[:] c= [:[:].(a - s),(a + s).[,].(b - s),(b + s).[:],].(c - s),(c + s).[:] by A52, ZFMISC_1:96;
hence ( 0 < r0 & r0 = F . [a,b,c] & [:].(a - r0),(a + r0).[,].(b - r0),(b + r0).[,].(c - r0),(c + r0).[:] c= A ) by A49, A51, A46, A48, XREAL_1:215; :: thesis: verum
end;
defpred S1[ object , object ] means ex a, b, c, r being Real ex E being set st
( p . $1 = [a,b,c] & a in RAT & b in RAT & c in RAT & 0 < r & r = F . [a,b,c] & E = $2 & E = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] & E c= A );
A53: for i being object st i in NAT holds
ex y being object st
( y in bool [:REAL,REAL,REAL:] & S1[i,y] )
proof
let i be object ; :: thesis: ( i in NAT implies ex y being object st
( y in bool [:REAL,REAL,REAL:] & S1[i,y] ) )
assume i in NAT ; :: thesis: ex y being object st
( y in bool [:REAL,REAL,REAL:] & S1[i,y] )
then i in dom p by FUNCT_2:def 1;
then p . i in rng p by FUNCT_1:3;
then A54: ( p . i in A & p . i in [:RAT,RAT,RAT:] ) by A44, XBOOLE_0:def 4;
then consider ab, c being object such that
A55: ( ab in [:RAT,RAT:] & c in RAT & p . i = [ab,c] ) by ZFMISC_1:def 2;
consider a, b being object such that
A56: ( a in RAT & b in RAT & ab = [a,b] ) by A55, ZFMISC_1:def 2;
reconsider a = a, b = b, c = c as Real by A55, A56;
consider r being Real such that
A57: ( 0 < r & r = F . [a,b,c] & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) by A45, A54, A55, A56;
set E = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:];
take y = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:]; :: thesis: ( y in bool [:REAL,REAL,REAL:] & S1[i,y] )
thus y in bool [:REAL,REAL,REAL:] ; :: thesis: S1[i,y]
thus S1[i,y] by A55, A56, A57; :: thesis: verum
end;
consider B being Function of NAT,(bool [:REAL,REAL,REAL:]) such that
A58: for i being object st i in NAT holds
S1[i,B . i] from FUNCT_2:sch 1(A53);
reconsider B = B as SetSequence of [:REAL,REAL,REAL:] ;
A59: for i being Nat ex a, b, c, r being Real st
( p . i = [a,b,c] & a in RAT & b in RAT & c in RAT & 0 < r & r = F . [a,b,c] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] & B . i c= A )
proof
let i be Nat; :: thesis: ex a, b, c, r being Real st
( p . i = [a,b,c] & a in RAT & b in RAT & c in RAT & 0 < r & r = F . [a,b,c] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] & B . i c= A )
ex a, b, c, r being Real ex E being set st
( p . i = [a,b,c] & a in RAT & b in RAT & c in RAT & 0 < r & r = F . [a,b,c] & E = B . i & E = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] & E c= A ) by A58, ORDINAL1:def 12;
hence ex a, b, c, r being Real st
( p . i = [a,b,c] & a in RAT & b in RAT & c in RAT & 0 < r & r = F . [a,b,c] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] & B . i c= A ) ; :: thesis: verum
end;
now :: thesis: for z being object st z in rng B holds
z in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
let z be object ; :: thesis: ( z in rng B implies z in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) )
assume z in rng B ; :: thesis: z in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
then consider i being Element of NAT such that
A60: ( i in dom B & z = B . i ) by PARTFUN1:3;
consider a, b, c, r being Real such that
A61: ( p . i = [a,b,c] & a in RAT & b in RAT & c in RAT & 0 < r & r = F . [a,b,c] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] & B . i c= A ) by A59;
A62: ( ].(a - r),(a + r).[ in L-Field & ].(b - r),(b + r).[ in L-Field & ].(c - r),(c + r).[ in L-Field ) by MEASUR10:5, MEASUR12:75;
then A63: [:].(a - r),(a + r).[,].(b - r),(b + r).[:] 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 A64: B . i in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) by A62, A61, A63;
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 z in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by A64, A60; :: thesis: verum
end;
then rng B c= sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) ;
then reconsider B = B as SetSequence of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by RELAT_1:def 19;
now :: thesis: for z being object st z in union (rng B) holds
z in A
let z be object ; :: thesis: ( z in union (rng B) implies z in A )
assume z in union (rng B) ; :: thesis: z in A
then consider Y being set such that
A65: ( z in Y & Y in rng B ) by TARSKI:def 4;
consider i being Element of NAT such that
A66: ( i in dom B & Y = B . i ) by A65, PARTFUN1:3;
ex a, b, c, r being Real st
( p . i = [a,b,c] & a in RAT & b in RAT & c in RAT & 0 < r & r = F . [a,b,c] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] & B . i c= A ) by A59;
hence z in A by A65, A66; :: thesis: verum
end;
then A67: union (rng B) c= A ;
now :: thesis: for z being object st z in A holds
z in union (rng B)
let z be object ; :: thesis: ( z in A implies z in union (rng B) )
assume A68: z in A ; :: thesis: z in union (rng B)
then reconsider u = z as Point of [:RNS_Real,RNS_Real,RNS_Real:] ;
consider e0 being Real such that
A69: ( e0 > 0 & Ball (u,e0) c= A ) by A68, A1, NDIFF_8:20;
set e1 = e0 / 2;
A70: ( 0 < e0 / 2 & e0 / 2 < e0 ) by A69, XREAL_1:215, XREAL_1:216;
set e = (e0 / 2) / 3;
( 0 < (e0 / 2) / 3 & (e0 / 2) / 3 < e0 / 2 ) by A70, XREAL_1:221, XREAL_1:222;
then A71: (e0 / 2) / 3 < e0 by A70, XXREAL_0:2;
then Ball (u,((e0 / 2) / 3)) c= Ball (u,e0) by NDIFF_8:15;
then A72: ( 0 < (e0 / 2) / 3 & Ball (u,((e0 / 2) / 3)) c= A ) by A69, A70, XREAL_1:222;
consider x1, y1, z1 being Point of RNS_Real such that
A73: u = [x1,y1,z1] by PRVECT_4:9;
reconsider xx1 = x1, yy1 = y1, zz1 = z1 as Real ;
A74: ( 0 < ((e0 / 2) / 3) / 2 & ((e0 / 2) / 3) / 2 < (e0 / 2) / 3 ) by A72, XREAL_1:215, XREAL_1:216;
A75: xx1 - (((e0 / 2) / 3) / 4) < xx1 by A72, XREAL_1:224, XREAL_1:44;
xx1 < xx1 + (((e0 / 2) / 3) / 4) by A72, XREAL_1:224, XREAL_1:29;
then xx1 - (((e0 / 2) / 3) / 4) < xx1 + (((e0 / 2) / 3) / 4) by A75, XXREAL_0:2;
then consider qx1 being Rational such that
A76: ( xx1 - (((e0 / 2) / 3) / 4) < qx1 & qx1 < xx1 + (((e0 / 2) / 3) / 4) ) by RAT_1:7;
qx1 in ].(xx1 - (((e0 / 2) / 3) / 4)),(xx1 + (((e0 / 2) / 3) / 4)).[ by A76;
then A77: |.(qx1 - xx1).| < ((e0 / 2) / 3) / 4 by RCOMP_1:1;
A78: yy1 - (((e0 / 2) / 3) / 4) < yy1 by A72, XREAL_1:224, XREAL_1:44;
yy1 < yy1 + (((e0 / 2) / 3) / 4) by A72, XREAL_1:224, XREAL_1:29;
then yy1 - (((e0 / 2) / 3) / 4) < yy1 + (((e0 / 2) / 3) / 4) by A78, XXREAL_0:2;
then consider qy1 being Rational such that
A79: ( yy1 - (((e0 / 2) / 3) / 4) < qy1 & qy1 < yy1 + (((e0 / 2) / 3) / 4) ) by RAT_1:7;
qy1 in ].(yy1 - (((e0 / 2) / 3) / 4)),(yy1 + (((e0 / 2) / 3) / 4)).[ by A79;
then A80: |.(qy1 - yy1).| < ((e0 / 2) / 3) / 4 by RCOMP_1:1;
A81: zz1 - (((e0 / 2) / 3) / 4) < zz1 by A72, XREAL_1:224, XREAL_1:44;
zz1 < zz1 + (((e0 / 2) / 3) / 4) by A72, XREAL_1:224, XREAL_1:29;
then zz1 - (((e0 / 2) / 3) / 4) < zz1 + (((e0 / 2) / 3) / 4) by A81, XXREAL_0:2;
then consider qz1 being Rational such that
A82: ( zz1 - (((e0 / 2) / 3) / 4) < qz1 & qz1 < zz1 + (((e0 / 2) / 3) / 4) ) by RAT_1:7;
qz1 in ].(zz1 - (((e0 / 2) / 3) / 4)),(zz1 + (((e0 / 2) / 3) / 4)).[ by A82;
then A83: |.(qz1 - zz1).| < ((e0 / 2) / 3) / 4 by RCOMP_1:1;
A84: ( qx1 in RAT & qy1 in RAT & qz1 in RAT ) by RAT_1:def 2;
reconsider dx1 = qx1, dy1 = qy1, dz1 = qz1 as Point of RNS_Real by XREAL_0:def 1;
dx1 - x1 = qx1 - xx1 by DUALSP03:4;
then A85: ||.(dx1 - x1).|| < ((e0 / 2) / 3) / 4 by A77, EUCLID:def 2;
dy1 - y1 = qy1 - yy1 by DUALSP03:4;
then A86: ||.(dy1 - y1).|| < ((e0 / 2) / 3) / 4 by A80, EUCLID:def 2;
dz1 - z1 = qz1 - zz1 by DUALSP03:4;
then A87: ||.(dz1 - z1).|| < ((e0 / 2) / 3) / 4 by A83, EUCLID:def 2;
reconsider v = [dx1,dy1,dz1] as Point of [:RNS_Real,RNS_Real,RNS_Real:] ;
A88: - v = [(- dx1),(- dy1),(- dz1)] by PRVECT_4:9;
u - v = [(x1 + (- dx1)),(y1 + (- dy1)),(z1 + (- dz1))] by A73, A88, PRVECT_4:9;
then ||.(u - v).|| <= (||.(x1 - dx1).|| + ||.(y1 - dy1).||) + ||.(z1 - dz1).|| by Th1;
then ||.(u - v).|| <= (||.(dx1 - x1).|| + ||.(y1 - dy1).||) + ||.(z1 - dz1).|| by NORMSP_1:7;
then ||.(u - v).|| <= (||.(dx1 - x1).|| + ||.(dy1 - y1).||) + ||.(z1 - dz1).|| by NORMSP_1:7;
then A89: ||.(u - v).|| <= (||.(dx1 - x1).|| + ||.(dy1 - y1).||) + ||.(dz1 - z1).|| by NORMSP_1:7;
||.(dx1 - x1).|| + ||.(dy1 - y1).|| <= (((e0 / 2) / 3) / 4) + (((e0 / 2) / 3) / 4) by A85, A86, XREAL_1:7;
then (||.(dx1 - x1).|| + ||.(dy1 - y1).||) + ||.(dz1 - z1).|| <= ((((e0 / 2) / 3) / 4) + (((e0 / 2) / 3) / 4)) + (((e0 / 2) / 3) / 4) by A87, XREAL_1:7;
then (||.(dx1 - x1).|| + ||.(dy1 - y1).||) + ||.(dz1 - z1).|| <= (((((e0 / 2) / 3) / 4) + (((e0 / 2) / 3) / 4)) + (((e0 / 2) / 3) / 4)) + (((e0 / 2) / 3) / 4) by A69, XREAL_1:38;
then ||.(u - v).|| <= (e0 / 2) / 3 by A89, XXREAL_0:2;
then ||.(u - v).|| < e0 by XXREAL_0:2, A71;
then A90: v in Ball (u,e0) ;
[qx1,qy1] in [:RAT,RAT:] by A84, ZFMISC_1:87;
then [qx1,qy1,qz1] in [:RAT,RAT,RAT:] by A84, ZFMISC_1:87;
then [qx1,qy1,qz1] in rng p by A44, A69, A90, XBOOLE_0:def 4;
then consider k being Element of NAT such that
A91: ( k in dom p & p . k = [qx1,qy1,qz1] ) by PARTFUN1:3;
consider Rx being real-membered set such that
A92: ( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(qx1 - r),(qx1 + r).[,].(qy1 - r),(qy1 + r).[,].(qz1 - r),(qz1 + r).[:] c= A ) } & F . [qx1,qy1,qz1] = (upper_bound Rx) / 2 ) by A69, A90, A23;
consider ak, bk, ck, rk being Real such that
A93: ( p . k = [ak,bk,ck] & ak in RAT & bk in RAT & ck in RAT & 0 < rk & rk = F . [ak,bk,ck] & B . k = [:].(ak - rk),(ak + rk).[,].(bk - rk),(bk + rk).[,].(ck - rk),(ck + rk).[:] & B . k c= A ) by A59;
A94: ( ak = qx1 & bk = qy1 & ck = qz1 ) by A91, A93, XTUPLE_0:3;
then A95: ( |.(xx1 - ak).| < ((e0 / 2) / 3) / 4 & |.(yy1 - bk).| < ((e0 / 2) / 3) / 4 & |.(zz1 - ck).| < ((e0 / 2) / 3) / 4 ) by A77, A80, A83, COMPLEX1:60;
set d = ((e0 / 2) / 3) / 4;
now :: thesis: for z being object st z in [:].(ak - (((e0 / 2) / 3) / 2)),(ak + (((e0 / 2) / 3) / 2)).[,].(bk - (((e0 / 2) / 3) / 2)),(bk + (((e0 / 2) / 3) / 2)).[,].(ck - (((e0 / 2) / 3) / 2)),(ck + (((e0 / 2) / 3) / 2)).[:] holds
z in A
let z be object ; :: thesis: ( z in [:].(ak - (((e0 / 2) / 3) / 2)),(ak + (((e0 / 2) / 3) / 2)).[,].(bk - (((e0 / 2) / 3) / 2)),(bk + (((e0 / 2) / 3) / 2)).[,].(ck - (((e0 / 2) / 3) / 2)),(ck + (((e0 / 2) / 3) / 2)).[:] implies z in A )
assume z in [:].(ak - (((e0 / 2) / 3) / 2)),(ak + (((e0 / 2) / 3) / 2)).[,].(bk - (((e0 / 2) / 3) / 2)),(bk + (((e0 / 2) / 3) / 2)).[,].(ck - (((e0 / 2) / 3) / 2)),(ck + (((e0 / 2) / 3) / 2)).[:] ; :: thesis: z in A
then consider s1, v being object such that
A96: ( s1 in [:].(ak - (((e0 / 2) / 3) / 2)),(ak + (((e0 / 2) / 3) / 2)).[,].(bk - (((e0 / 2) / 3) / 2)),(bk + (((e0 / 2) / 3) / 2)).[:] & v in ].(ck - (((e0 / 2) / 3) / 2)),(ck + (((e0 / 2) / 3) / 2)).[ & z = [s1,v] ) by ZFMISC_1:def 2;
consider s, t being object such that
A97: ( s in ].(ak - (((e0 / 2) / 3) / 2)),(ak + (((e0 / 2) / 3) / 2)).[ & t in ].(bk - (((e0 / 2) / 3) / 2)),(bk + (((e0 / 2) / 3) / 2)).[ & s1 = [s,t] ) by A96, ZFMISC_1:def 2;
reconsider s = s, t = t, v = v as Real by A96, A97;
reconsider ss = s, tt = t, vv = v as Point of RNS_Real by XREAL_0:def 1;
reconsider w = [ss,tt,vv] as Point of [:RNS_Real,RNS_Real,RNS_Real:] ;
( |.(s - ak).| < ((e0 / 2) / 3) / 2 & |.(t - bk).| < ((e0 / 2) / 3) / 2 & |.(v - ck).| < ((e0 / 2) / 3) / 2 ) by A96, A97, RCOMP_1:1;
then A98: ( |.(ak - s).| < ((e0 / 2) / 3) / 2 & |.(bk - t).| < ((e0 / 2) / 3) / 2 & |.(ck - v).| < ((e0 / 2) / 3) / 2 ) by COMPLEX1:60;
(((e0 / 2) / 3) / 2) / 2 < ((e0 / 2) / 3) / 2 by A72, XREAL_1:215, XREAL_1:216;
then A99: ( |.(xx1 - ak).| < ((e0 / 2) / 3) / 2 & |.(yy1 - bk).| < ((e0 / 2) / 3) / 2 & |.(zz1 - ck).| < ((e0 / 2) / 3) / 2 ) by A95, XXREAL_0:2;
A100: |.(xx1 - s).| <= |.(xx1 - ak).| + |.(ak - s).| by COMPLEX1:63;
|.(xx1 - ak).| + |.(ak - s).| <= (((e0 / 2) / 3) / 2) + (((e0 / 2) / 3) / 2) by A98, A99, XREAL_1:7;
then A101: |.(xx1 - s).| <= (e0 / 2) / 3 by A100, XXREAL_0:2;
A102: |.(yy1 - t).| <= |.(yy1 - bk).| + |.(bk - t).| by COMPLEX1:63;
|.(yy1 - bk).| + |.(bk - t).| <= (((e0 / 2) / 3) / 2) + (((e0 / 2) / 3) / 2) by A98, A99, XREAL_1:7;
then A103: |.(yy1 - t).| <= (e0 / 2) / 3 by A102, XXREAL_0:2;
A104: |.(zz1 - v).| <= |.(zz1 - ck).| + |.(ck - v).| by COMPLEX1:63;
|.(zz1 - ck).| + |.(ck - v).| <= (((e0 / 2) / 3) / 2) + (((e0 / 2) / 3) / 2) by A98, A99, XREAL_1:7;
then A105: |.(zz1 - v).| <= (e0 / 2) / 3 by A104, XXREAL_0:2;
x1 - ss = xx1 - s by DUALSP03:4;
then A106: ||.(x1 - ss).|| <= (e0 / 2) / 3 by A101, EUCLID:def 2;
y1 - tt = yy1 - t by DUALSP03:4;
then A107: ||.(y1 - tt).|| <= (e0 / 2) / 3 by A103, EUCLID:def 2;
z1 - vv = zz1 - v by DUALSP03:4;
then A108: ||.(z1 - vv).|| <= (e0 / 2) / 3 by A105, EUCLID:def 2;
A109: - w = [(- ss),(- tt),(- vv)] by PRVECT_4:9;
u - w = [(x1 + (- ss)),(y1 + (- tt)),(z1 + (- vv))] by A109, A73, PRVECT_4:9;
then A110: ||.(u - w).|| <= (||.(x1 - ss).|| + ||.(y1 - tt).||) + ||.(z1 - vv).|| by Th1;
||.(x1 - ss).|| + ||.(y1 - tt).|| <= ((e0 / 2) / 3) + ((e0 / 2) / 3) by A106, A107, XREAL_1:7;
then (||.(x1 - ss).|| + ||.(y1 - tt).||) + ||.(z1 - vv).|| <= (((e0 / 2) / 3) + ((e0 / 2) / 3)) + ((e0 / 2) / 3) by A108, XREAL_1:7;
then A111: ||.(u - w).|| <= e0 / 2 by A110, XXREAL_0:2;
e0 / 2 < e0 by A69, XREAL_1:216;
then ||.(u - w).|| < e0 by A111, XXREAL_0:2;
then w in Ball (u,e0) ;
hence z in A by A96, A97, A69; :: thesis: verum
end;
then [:].(ak - (((e0 / 2) / 3) / 2)),(ak + (((e0 / 2) / 3) / 2)).[,].(bk - (((e0 / 2) / 3) / 2)),(bk + (((e0 / 2) / 3) / 2)).[,].(ck - (((e0 / 2) / 3) / 2)),(ck + (((e0 / 2) / 3) / 2)).[:] c= A ;
then ((e0 / 2) / 3) / 2 in Rx by A74, A92, A94;
then ((e0 / 2) / 3) / 2 <= upper_bound Rx by A92, SEQ_4:def 1;
then (((e0 / 2) / 3) / 2) / 2 <= (upper_bound Rx) / 2 by XREAL_1:72;
then ( ].(ak - (((e0 / 2) / 3) / 4)),(ak + (((e0 / 2) / 3) / 4)).[ c= ].(ak - rk),(ak + rk).[ & ].(bk - (((e0 / 2) / 3) / 4)),(bk + (((e0 / 2) / 3) / 4)).[ c= ].(bk - rk),(bk + rk).[ & ].(ck - (((e0 / 2) / 3) / 4)),(ck + (((e0 / 2) / 3) / 4)).[ c= ].(ck - rk),(ck + rk).[ ) by A92, A93, Lm2, A91;
then A112: ( x1 in ].(ak - rk),(ak + rk).[ & y1 in ].(bk - rk),(bk + rk).[ & z1 in ].(ck - rk),(ck + rk).[ ) by A95, RCOMP_1:1;
then [x1,y1] in [:].(ak - rk),(ak + rk).[,].(bk - rk),(bk + rk).[:] by ZFMISC_1:87;
then A113: u in B . k by A93, A73, A112, ZFMISC_1:87;
k in NAT ;
then k in dom B by FUNCT_2:def 1;
then B . k in rng B by FUNCT_1:3;
hence z in union (rng B) by A113, TARSKI:def 4; :: thesis: verum
end;
then A c= union (rng B) ;
then Union B = A by A67, CARD_3:def 4;
hence A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) by PROB_1:17; :: thesis: verum
end;
end;
end;
end;