let a, b be Real; :: thesis: ( a < b implies ex E being SetSequence of L-Field st
( ( for n being Nat holds
( E . n = [.(a + ((b - a) / (n + 1))),b.] & E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL ) ) & E is non-descending & E is convergent & Union E = ].a,b.] ) )
assume A1: a < b ; :: thesis: ex E being SetSequence of L-Field st
( ( for n being Nat holds
( E . n = [.(a + ((b - a) / (n + 1))),b.] & E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL ) ) & E is non-descending & E is convergent & Union E = ].a,b.] )
deffunc H₁( Element of NAT ) -> Element of bool REAL = [.(a + ((b - a) / ($1 + 1))),b.];
consider E being Function of NAT,(bool REAL) such that
A2: for n being Element of NAT holds E . n = H₁(n) from FUNCT_2:sch 4();

now :: thesis: for x being object st x in rng E holds
x in L-Field

let x be object ; :: thesis: ( x in rng E implies x in L-Field )
assume x in rng E ; :: thesis: x in L-Field
then consider n being object such that
A3: ( n in dom E & E . n = x ) by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A3;
E . n = [.(a + ((b - a) / (n + 1))),b.] by A2;
hence x in L-Field by A3, MEASUR10:5, MEASUR12:75; :: thesis: verum

end;

then rng E c= L-Field ;
then reconsider E = E as SetSequence of L-Field by RELAT_1:def 19;
take E ; :: thesis: ( ( for n being Nat holds
( E . n = [.(a + ((b - a) / (n + 1))),b.] & E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL ) ) & E is non-descending & E is convergent & Union E = ].a,b.] )
thus for n being Nat holds
( E . n = [.(a + ((b - a) / (n + 1))),b.] & E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL ) :: thesis: ( E is non-descending & E is convergent & Union E = ].a,b.] )

proof

let n be Nat; :: thesis: ( E . n = [.(a + ((b - a) / (n + 1))),b.] & E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL )
n is Element of NAT by ORDINAL1:def 12;
hence A4: E . n = [.(a + ((b - a) / (n + 1))),b.] by A2; :: thesis: ( E . n c= ].a,b.] & E . n is non empty closed_interval Subset of REAL )
A5: ( a < a + ((b - a) / (n + 1)) & a + ((b - a) / (n + 1)) <= b ) by A1, Th22;
hence E . n c= ].a,b.] by A4, XXREAL_1:39; :: thesis: E . n is non empty closed_interval Subset of REAL
thus E . n is non empty closed_interval Subset of REAL by A4, A5, XXREAL_1:30, MEASURE5:def 3; :: thesis: verum

end;

hence ( E is non-descending & E is convergent & Union E = ].a,b.] ) by A1, Lm4; :: thesis: verum