theorem Th24: :: MESFUN15:22

for a, b being Real st a < b holds
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.] )