for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T st Y in NetUniv T & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T