let IT be Subset of REAL; :: thesis: ( IT is closed_interval implies IT is compact )
assume IT is closed_interval ; :: thesis: IT is compact
then ex a, b being Real st IT = [.a,b.] by MEASURE5:def 3;
hence IT is compact by RCOMP_1:6; :: thesis: verum