set A = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #);
A1:
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 N, the InternalRel of N #)
;
[#] N is directed
by WAYBEL_0:def 6;
then
[#] NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is directed
by A1, WAYBEL_0:3;
then reconsider A = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as net of T by A1, WAYBEL_0:def 6, WAYBEL_8:13;
A is subnet of N
then reconsider A = A as subnet of N ;
take
A
; A is strict
thus
A is strict
; verum