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