:: deftheorem defines = INTERVA1:def 7 :
for U being non empty set
for A, B being non empty IntervalSet of U holds
( A = B iff ( A ``1 = B ``1 & A ``2 = B ``2 ) );