:: deftheorem Def4000 defines ext_left_closed_sets FINANCE5:def 16 :
for b being Real
for b₂ being SetSequence of ExtREAL holds
( b₂ = ext_left_closed_sets b iff for n being Nat holds b₂ . n = [.(b + n),+infty.] );