let S be 1-sorted ; :: thesis: for R being NetStr of S holds NetStr(# the carrier of R,the InternalRel of R,the mapping of R #) is full SubRelStr of R
let R be NetStr of S; :: thesis: NetStr(# the carrier of R,the InternalRel of R,the mapping of R #) is full SubRelStr of R
reconsider R' = NetStr(# the carrier of R,the InternalRel of R,the mapping of R #) as SubRelStr of R by YELLOW_0:def 13;
the InternalRel of R' = the InternalRel of R |_2 the carrier of R' by XBOOLE_1:28;
hence NetStr(# the carrier of R,the InternalRel of R,the mapping of R #) is full SubRelStr of R by YELLOW_0:def 14; :: thesis: verum