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