:: deftheorem Def23 defines (ITERATED_LIMITS) YELLOW_6:def 23 :
for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (ITERATED_LIMITS) iff for X being net of T
for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C );