let M be non empty MetrSpace; :: thesis: for F, G being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds
L is Lebesgue_number of G
let F, G be open Subset-Family of (TopSpaceMetr M); :: thesis: for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds
L is Lebesgue_number of G
let L be Lebesgue_number of F; :: thesis: ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G implies L is Lebesgue_number of G )
assume that
A1: TopSpaceMetr M is compact and
A2: F is Cover of (TopSpaceMetr M) and
A3: F c= G ; :: thesis: L is Lebesgue_number of G

A4: now :: thesis: for x being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in G & Ball (x,L) c= A )

let x be Point of M; :: thesis: ex A being Subset of (TopSpaceMetr M) st
( A in G & Ball (x,L) c= A )
ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (x,L) c= A ) by A1, A2, Def1;
hence ex A being Subset of (TopSpaceMetr M) st
( A in G & Ball (x,L) c= A ) by A3; :: thesis: verum

end;

set TM = TopSpaceMetr M;
( union F = [#] (TopSpaceMetr M) & union F c= union G ) by A2, A3, SETFAM_1:45, ZFMISC_1:77;
then G is Cover of (TopSpaceMetr M) by SETFAM_1:def 11;
hence L is Lebesgue_number of G by A1, A4, Def1; :: thesis: verum