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
A1: N is SubRelStr of N by Th15;
the mapping of N = the mapping of N | the carrier of N by RELSET_1:34;
hence N is SubNetStr of N by A1, Def8; :: thesis: verum