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