let N be Subset of REAL; :: thesis: ( 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 ) )
reconsider M = N as Subset of R^1 ;
( M 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 ) ) by Th27;
hence ( 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 ) ) by JORDAN5A:25; :: thesis: verum