for X being non empty MetrSpace
for S being sequence of X st S is constant holds
S is Cauchy by Th23, TBSP_1:5;