set S = NetStr(# the carrier of N,the InternalRel of N,the mapping of N #);
A1: ( N is SubNetStr of N & RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of N,the InternalRel of N #) & RelStr(# the carrier of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #),the InternalRel of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) #) = RelStr(# the carrier of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #),the InternalRel of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) #) & N is full SubRelStr of N ) by YELLOW_6:15, YELLOW_6:17;
then ( the mapping of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) = the mapping of N | the carrier of NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) & NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) is full SubRelStr of N ) by WAYBEL21:12, YELLOW_6:def 8;
then reconsider S = NetStr(# the carrier of N,the InternalRel of N,the mapping of N #) as non empty strict full SubNetStr of N by YELLOW_6:def 8, YELLOW_6:def 9;
S is directed

proof

( [#] N = the carrier of N & [#] S = the carrier of S & [#] N is directed ) by WAYBEL_0:def 6;
hence [#] S is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def 6 :: thesis: verum

end;

hence ex b₁ being SubNetStr of N st
( b₁ is strict & not b₁ is empty & b₁ is directed & b₁ is full ) ; :: thesis: verum