for N being non empty MetrSpace
for G being Subset-Family of (TopSpaceMetr N) st G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact holds
ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )