let S be 1-sorted ; :: thesis: for N being NetStr over S holds N is SubNetStr of N
let N be NetStr over 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 Th6;
hence N is SubNetStr of N by Def6; :: thesis: verum