:: deftheorem Def10 defines " YELLOW_6:def 10 :
for S being 1-sorted
for N being NetStr over S
for X being set
for b₄ being strict SubNetStr of N holds
( b₄ = N " X iff ( b₄ is full SubRelStr of N & the carrier of b₄ = the mapping of N " X ) );