:: deftheorem defines open_interval MEASURE5:def 2 :
for IT being Subset of REAL holds
( IT is open_interval iff ex a, b being R_eal st IT = ].a,b.[ );