:: deftheorem Def1 defines half_open_sets FINANCE1:def 1 :
for a, b being Real
for b₃ being SetSequence of REAL holds
( b₃ = half_open_sets (a,b) iff ( b₃ . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds b₃ . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) ) );