theorem :: YELLOW_6:8

for S being 1-sorted
for N being NetStr over S holds N is SubNetStr of N