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