:: deftheorem Def15 defines complete LOPBAN_1:def 15 :
for X being RealNormSpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent );