let S be 1-sorted ; :: thesis: for N being NetStr over S
for M being SubNetStr of N holds the carrier of M c= the carrier of N
let N be NetStr over S; :: thesis: for M being SubNetStr of N holds the carrier of M c= the carrier of N
let M be SubNetStr of N; :: thesis: the carrier of M c= the carrier of N
M is SubRelStr of N by Def6;
hence the carrier of M c= the carrier of N by YELLOW_0:def 13; :: thesis: verum