:: deftheorem defines complete TBSP_1:def 5 :
for N being non empty MetrStruct holds
( N is complete iff for S2 being sequence of N st S2 is Cauchy holds
S2 is convergent );