:: deftheorem Def3000 defines ext_right_closed_sets FINANCE5:def 15 :
for b being Real
for b₂ being SetSequence of ExtREAL holds
( b₂ = ext_right_closed_sets b iff for n being Nat holds b₂ . n = [.-infty,(b - n).] );