theorem Th25: :: MESFUN15:23

for a being Real 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.[ )