reconsider M = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as SubNetStr of N by Lm4;
take M ; :: thesis: ( M is full & M is strict )
thus M is full SubRelStr of N by Lm5; :: according to YELLOW_6:def 7 :: thesis: M is strict
thus M is strict ; :: thesis: verum