:: deftheorem Def11 defines IntervalSets INTERVA1:def 11 :
for U, b₂ being non empty set holds
( b₂ = IntervalSets U iff for x being set holds
( x in b₂ iff x is non empty IntervalSet of U ) );