let S be 1-sorted ; :: thesis: for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is SubNetStr of R
let N be NetStr over 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 YELLOW_0:def 13;
hence NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is SubNetStr of N by Def6; :: thesis: verum