theorem Th29: :: COMPL_SP:30

for M being non empty Reflexive symmetric MetrStruct
for r being Real st r > 0 holds
ex A being Subset of M st
( ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) & ( for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) ) ) )