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 7 :: thesis: I is interval
hence I is interval ; :: thesis: verum