set S = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #);
A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N, the InternalRel of N #) ;
N is full SubRelStr of N by YELLOW_6:6;
then A2: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is full SubRelStr of N by A1, WAYBEL21:12;
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 #) ;
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 A2, YELLOW_6:def 6, YELLOW_6:def 7;
[#] N is directed by WAYBEL_0:def 6;
then [#] S is directed by A1, WAYBEL_0:3;
then S is directed ;
hence ex b₁ being SubNetStr of N st
( b₁ is strict & not b₁ is empty & b₁ is directed & b₁ is full ) ; :: thesis: verum