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 - ((b - a) / (n + 1))).] & 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 - ((b - a) / (n + 1))).] & 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 - ((b - a) / ($1 + 1))).];
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 - ((b - a) / (n + 1))).] 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 - ((b - a) / (n + 1))).] & 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.[ )
A4: for n being Nat holds E . n = [.a,(b - ((b - a) / (n + 1))).]

proof

let n be Nat; :: thesis: E . n = [.a,(b - ((b - a) / (n + 1))).]
n is Element of NAT by ORDINAL1:def 12;
hence E . n = [.a,(b - ((b - a) / (n + 1))).] by A2; :: thesis: verum

end;

thus for n being Nat holds
( E . n = [.a,(b - ((b - a) / (n + 1))).] & 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 - ((b - a) / (n + 1))).] & E . n c= [.a,b.[ & E . n is non empty closed_interval Subset of REAL )
thus E . n = [.a,(b - ((b - a) / (n + 1))).] by A4; :: thesis: ( E . n c= [.a,b.[ & E . n is non empty closed_interval Subset of REAL )
A5: E . n = [.a,(b - ((b - a) / (n + 1))).] by A4;
A6: b - ((b - a) / (n + 1)) < b by A1, Th22;
a <= b - ((b - a) / (n + 1)) by A1, Th22;
hence ( E . n c= [.a,b.[ & E . n is non empty closed_interval Subset of REAL ) by A5, A6, MEASURE5:def 3, XXREAL_1:30, XXREAL_1:43; :: thesis: verum

end;

thus ( E is non-descending & E is convergent & Union E = [.a,b.[ ) by A1, A4, Lm3; :: thesis: verum