theorem Th40: :: COMPL_SP:41

for X being set
for M being non empty Reflexive symmetric triangle MetrStruct
for a being Point of M
for S being sequence of (WellSpace (a,X)) holds
( not S is Cauchy or for Xa being Point of (WellSpace (a,X)) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S . m = [Y,p] )