:: deftheorem Def6 defines ``2 INTERVA1:def 6 :
for U being non empty set
for A being non empty IntervalSet of U
for b<sub>3</sub> being Subset of U holds
( b<sub>3</sub> = A ``2 iff ex B being Subset of U st A = Inter (B,b₃) );