for M being non empty MetrSpace
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