:: deftheorem Def12 defines net_set YELLOW_6:def 12 :
for X being set
for T being 1-sorted
for b₃ being ManySortedSet of X holds
( b₃ is net_set of X,T iff for i being set st i in rng b₃ holds
i is net of T );