let Q be 1-sorted ; :: thesis: for R being NetStr over Q
for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
let R be NetStr over Q; :: thesis: for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
let S be SubNetStr of R; :: thesis: for T being SubNetStr of S holds T is SubNetStr of R
let T be SubNetStr of S; :: thesis: T is SubNetStr of R
A1: T is SubRelStr of S by Def6;
then A2: the carrier of T c= the carrier of S by YELLOW_0:def 13;
A3: the mapping of T = the mapping of S | the carrier of T by Def6
.= ( the mapping of R | the carrier of S) | the carrier of T by Def6
.= the mapping of R | ( the carrier of S /\ the carrier of T) by RELAT_1:71
.= the mapping of R | the carrier of T by A2, XBOOLE_1:28 ;
S is SubRelStr of R by Def6;
then T is SubRelStr of R by A1, Th7;
hence T is SubNetStr of R by A3, Def6; :: thesis: verum