let S be 1-sorted ; :: thesis: for N being NetStr of S holds N is SubNetStr of N
let N be NetStr of S; :: thesis: N is SubNetStr of N
( N is SubRelStr of N & the mapping of N = the mapping of N | the carrier of N ) by Th15, RELSET_1:19;
hence N is SubNetStr of N by Def8; :: thesis: verum