:: deftheorem defines ^ INTERVA1:def 10 :
for U being non empty set
for A being non empty IntervalSet of U holds A ^ = (Inter (([#] U),([#] U))) _\_ A;