let a be Real; :: thesis: ex E being SetSequence of L-Field st
( ( for n being Nat holds E . n = [.a,(a + n).] ) & E is non-descending & E is convergent & Union E = [.a,+infty.[ )
deffunc H₁( Element of NAT ) -> Element of bool REAL = [.a,(a + $1).];
consider E being Function of NAT,(bool REAL) such that
A1: 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
A2: ( n in dom E & E . n = x ) by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A2;
E . n = [.a,(a + n).] by A1;
hence x in L-Field by A2, 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,(a + n).] ) & E is non-descending & E is convergent & Union E = [.a,+infty.[ )
thus for n being Nat holds E . n = [.a,(a + n).] :: thesis: ( E is non-descending & E is convergent & Union E = [.a,+infty.[ )

proof

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

end;

hence ( E is non-descending & E is convergent & Union E = [.a,+infty.[ ) by Lm5; :: thesis: verum