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:19, 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