let X be Subset of REAL; :: thesis: ( X = [.a,b.] implies X is closed_interval )
assume X = [.a,b.] ; :: thesis: X is closed_interval
hence ex x, y being Real st X = [.x,y.] ; :: according to MEASURE5:def 3 :: thesis: verum