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 & not M is empty & M is strict )
thus M is full SubRelStr of N by Lm5; :: according to YELLOW_6:def 7 :: thesis: ( not M is empty & M is strict )
thus ( not M is empty & M is strict ) ; :: thesis: verum