:: deftheorem Def2 defines Subset YELLOW19:def 2 :
for S being non empty 1-sorted
for N being non empty NetStr over S
for b₃ being Subset of S holds
( b₃ is Subset of S,N iff ex i being Element of N st b₃ = rng the mapping of (N | i) );