let I be Subset of REAL; :: thesis: ( I is closed_interval implies I is interval )
assume ex a, b being real number st I = [.a,b.] ; :: according to MEASURE5:def 3 :: thesis: I is interval
hence I is interval ; :: thesis: verum