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