theorem :: COMPL_SP:14

for M being non empty MetrSpace holds
( M is complete iff for F being Subset-Family of (TopSpaceMetr M) st F is closed & F is centered & ( for r being Real st r > 0 holds
ex A being Subset of M st
( A in F & A is bounded & diameter A < r ) ) holds
not meet F is empty )