:: deftheorem defines Family_of_Intervals MEASUR10:def 1 :
Family_of_Intervals = { I where I is Interval : verum } ;