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