theorem Th26: :: MESFUN15:24

for a being Real ex E being SetSequence of L-Field st
( ( for n being Nat holds E . n = [.(a - n),a.] ) & E is non-descending & E is convergent & Union E = ].-infty,a.] )