theorem :: TOPMETR4:24

for N being Subset of REAL holds
( N is compact iff for F being Subset-Family of REAL st F is Cover of N & ( for P being Subset of REAL st P in F holds
P is open ) holds
ex G being Subset-Family of REAL st
( G c= F & G is Cover of N & G is finite ) )