:: deftheorem Def2 defines IntervalSet INTERVA1:def 2 :
for U being set
for b₂ being Subset-Family of U holds
( b₂ is IntervalSet of U iff ex A, B being Subset of U st b₂ = Inter (A,B) );