:: deftheorem Def300 defines ext_half_open_sets FINANCE5:def 14 :
for b being Real
for b₂ being SetSequence of ExtREAL holds
( b₂ = ext_half_open_sets b iff ( b₂ . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b₂ . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) ) );