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 is_finer_than 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 is_finer_than 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 is_finer_than 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 is_finer_than G ; :: thesis: L is Lebesgue_number of G
set TM = TopSpaceMetr M;

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

let x be Point of M; :: thesis: ex B being Subset of (TopSpaceMetr M) st
( B in G & Ball (x,L) c= B )
consider A being Subset of (TopSpaceMetr M) such that
A5: A in F and
A6: Ball (x,L) c= A by A1, A2, Def1;
consider B being set such that
A7: B in G and
A8: A c= B by A3, A5, SETFAM_1:def 2;
reconsider B = B as Subset of (TopSpaceMetr M) by A7;
take B = B; :: thesis: ( B in G & Ball (x,L) c= B )
thus ( B in G & Ball (x,L) c= B ) by A6, A7, A8; :: thesis: verum

end;

( union F = [#] (TopSpaceMetr M) & union F c= union G ) by A2, A3, SETFAM_1:13, SETFAM_1:45;
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