let I, J be closed_interval Subset of REAL; :: thesis: for E being Subset of [:RNS_Real,RNS_Real:] st E = [:I,J:] holds
E is compact
let E be Subset of [:RNS_Real,RNS_Real:]; :: thesis: ( E = [:I,J:] implies E is compact )
assume A1: E = [:I,J:] ; :: thesis: E is compact
reconsider A = I, B = J as Subset of RNS_Real ;
( A is compact & B is compact ) by Th7;
hence E is compact by A1, Th8; :: thesis: verum