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