let Q be 1-sorted ; :: thesis: for R being NetStr of Q
for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
let R be NetStr of 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 Def8;
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 Def8
.= (the mapping of R | the carrier of S) | the carrier of T by Def8
.= the mapping of R | (the carrier of S /\ the carrier of T) by RELAT_1:100
.= the mapping of R | the carrier of T by A2, XBOOLE_1:28 ;
S is SubRelStr of R by Def8;
then T is SubRelStr of R by A1, Th16;
hence T is SubNetStr of R by A3, Def8; :: thesis: verum