theorem Th24: :: YELLOW_6:24

for X being set
for T being 1-sorted
for F being ManySortedSet of X holds
( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )