let M be non empty MetrSpace; :: thesis: for F being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F
for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds
L1 is Lebesgue_number of F
let F be open Subset-Family of (TopSpaceMetr M); :: thesis: for L being Lebesgue_number of F
for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds
L1 is Lebesgue_number of F
let L be Lebesgue_number of F; :: thesis: for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds
L1 is Lebesgue_number of F
let L9 be positive Real; :: thesis: ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L9 <= L implies L9 is Lebesgue_number of F )
assume that
A1: ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) ) and
A2: L9 <= L ; :: thesis: L9 is Lebesgue_number of F

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

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

end;

hence L9 is Lebesgue_number of F by A1, Def1; :: thesis: verum