theorem Th23: :: MESFUN15:21

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 - ((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.[ )