:: deftheorem defines _\/_ INTERVA1:def 4 :
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = UNION (A,B);