let I, J, K be closed_interval Subset of REAL; :: thesis: for E being Subset of [:[:RNS_Real,RNS_Real:],RNS_Real:] st E = [:[:I,J:],K:] holds
E is compact
let E be Subset of [:[:RNS_Real,RNS_Real:],RNS_Real:]; :: thesis: ( E = [:[:I,J:],K:] implies E is compact )
assume A1: E = [:[:I,J:],K:] ; :: thesis: E is compact
set S = [:[:RNS_Real,RNS_Real:],RNS_Real:];
reconsider AB = [:I,J:] as Subset of [:RNS_Real,RNS_Real:] ;
reconsider C = K as Subset of RNS_Real ;
( AB is compact & C is compact ) by MESFUN16:7, MESFUN16:9;
hence E is compact by A1, MESFUN16:8; :: thesis: verum