for X being RealUnitarySpace
for seq being sequence of X st X is complete & seq is Cauchy holds
seq is bounded