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_{1} being SubNetStr of N st

( b_{1} is strict & not b_{1} is empty & b_{1} is directed & b_{1} is full )
; :: thesis: verum

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

( b