theorem Th21: :: RUSUB_7:21

for X being RealUnitarySpace
for M being non empty Subset of X
for seq being sequence of X st rng seq c= the carrier of (Ort_Comp M) & seq is convergent holds
lim seq in the carrier of (Ort_Comp M)