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