let A be closed-interval Subset of REAL ; :: thesis: A is compact
ex a, b being Real st
( a <= b & A = [.a,b.] ) by Def1;
hence A is compact by RCOMP_1:24; :: thesis: verum