:: deftheorem Def8 defines closed COMPL_SP:def 8 :
for M being MetrStruct
for S being SetSequence of M holds
( S is closed iff for i being Nat holds S . i is closed );