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;
S is SubRelStr of R by Def8;
then A2: T is SubRelStr of R by A1, Th16;
A3: the carrier of T c= the carrier of S by A1, YELLOW_0:def 13;
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 A3, XBOOLE_1:28 ;
hence T is SubNetStr of R by A2, Def8; :: thesis: verum