theorem :: YELLOW_6:9

for Q being 1-sorted
for R being NetStr over Q
for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R