theorem Th27: :: TOPMETR4:23

for N being Subset of REAL
for M being Subset of R^1 st N = M holds
( ( 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 ) ) iff for F1 being Subset-Family of R^1 st F1 is Cover of M & F1 is open holds
ex G1 being Subset-Family of R^1 st
( G1 c= F1 & G1 is Cover of M & G1 is finite ) )