:: deftheorem Def6 defines closed COMPL_SP:def 6 :
for T being TopStruct
for S being SetSequence of T holds
( S is closed iff for i being Nat holds S . i is closed );