:: deftheorem Def1 defines IntervalSequence COUSIN:def 1 :
for a, b being Real_Sequence
for b₃ being SetSequence of (REAL 1) holds
( b₃ = IntervalSequence (a,b) iff ex f being Function of NAT,(bool (REAL 1)) st
( b₃ = f & ( for i being Nat holds f . i = product <*[.(a . i),(b . i).]*> ) ) );