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
( NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) is SubRelStr of N & 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, YELLOW_0:def 13;
hence NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) is SubNetStr of N by Def8; :: thesis: verum