let S be 1-sorted ; :: thesis: for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
let R be NetStr over S; :: thesis: NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
reconsider R9 = 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 R9 = the InternalRel of R |_2 the carrier of R9 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