let S be 1-sorted ; :: thesis: for R being NetStr of S holds NetStr(# the carrier of R,the InternalRel of R,the mapping of R #) is SubNetStr of R
let N be NetStr of S; :: thesis: NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) is SubNetStr of N
A1: NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) is SubRelStr of N by YELLOW_0:def 13;
the mapping of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) = the mapping of N | the carrier of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) by RELSET_1:34;
hence NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) is SubNetStr of N by A1, Def8; :: thesis: verum