let N be Subset of REAL; :: thesis: 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 ) )
let M be Subset of R^1; :: thesis: ( N = M implies ( ( 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 ) ) )
assume A1: N = M ; :: thesis: ( ( 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 ) )
hereby :: thesis: ( ( 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 ) ) implies 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 ) )
assume A2: 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 ) ; :: thesis: 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 )
thus 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 ) :: thesis: verum
proof
let F1 be Subset-Family of R^1; :: thesis: ( F1 is Cover of M & F1 is open implies ex G1 being Subset-Family of R^1 st
( G1 c= F1 & G1 is Cover of M & G1 is finite ) )
assume A3: ( F1 is Cover of M & F1 is open ) ; :: thesis: ex G1 being Subset-Family of R^1 st
( G1 c= F1 & G1 is Cover of M & G1 is finite )
reconsider F = F1 as Subset-Family of REAL ;
for P being Subset of REAL st P in F holds
P is open
proof
let P be Subset of REAL; :: thesis: ( P in F implies P is open )
assume A4: P in F ; :: thesis: P is open
reconsider P1 = P as Subset of R^1 ;
P1 is open by A3, A4;
hence P is open by BORSUK_5:39; :: thesis: verum
end;
then consider G being Subset-Family of REAL such that
A5: ( G c= F & G is Cover of N & G is finite ) by A1, A2, A3;
reconsider G1 = G as Subset-Family of R^1 ;
take G1 ; :: thesis: ( G1 c= F1 & G1 is Cover of M & G1 is finite )
thus ( G1 c= F1 & G1 is Cover of M & G1 is finite ) by A1, A5; :: thesis: verum
end;
end;
assume A6: 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 ) ; :: thesis: 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 )
let F be Subset-Family of REAL; :: thesis: ( F is Cover of N & ( for P being Subset of REAL st P in F holds
P is open ) implies ex G being Subset-Family of REAL st
( G c= F & G is Cover of N & G is finite ) )
assume that
A7: F is Cover of N and
A8: for P being Subset of REAL st P in F holds
P is open ; :: thesis: ex G being Subset-Family of REAL st
( G c= F & G is Cover of N & G is finite )
reconsider F1 = F as Subset-Family of R^1 ;
for P1 being Subset of R^1 st P1 in F1 holds
P1 is open
proof
let P1 be Subset of R^1; :: thesis: ( P1 in F1 implies P1 is open )
assume A9: P1 in F1 ; :: thesis: P1 is open
reconsider P = P1 as Subset of REAL ;
P is open by A8, A9;
hence P1 is open by BORSUK_5:39; :: thesis: verum
end;
then F1 is open ;
then consider G1 being Subset-Family of R^1 such that
A10: ( G1 c= F1 & G1 is Cover of M & G1 is finite ) by A1, A6, A7;
reconsider G = G1 as Subset-Family of REAL ;
take G ; :: thesis: ( G c= F & G is Cover of N & G is finite )
thus ( G c= F & G is Cover of N & G is finite ) by A1, A10; :: thesis: verum