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

proof

reconsider f = id N as Function of A,N ;
take f ; :: according to YELLOW_6:def 9 :: thesis: ( the mapping of A = the mapping of N * f & ( for b₁ being Element of the carrier of N ex b₂ being Element of the carrier of A st
for b₃ being Element of the carrier of A holds
( not b₂ <= b₃ or b₁ <= f . b₃ ) ) )
thus the mapping of A = the mapping of N * f by FUNCT_2:17; :: thesis: for b₁ being Element of the carrier of N ex b₂ being Element of the carrier of A st
for b₃ being Element of the carrier of A holds
( not b₂ <= b₃ or b₁ <= f . b₃ )
let m be Element of N; :: thesis: ex b₁ being Element of the carrier of A st
for b₂ being Element of the carrier of A holds
( not b₁ <= b₂ or m <= f . b₂ )
reconsider n = m as Element of A ;
take n ; :: thesis: for b₁ being Element of the carrier of A holds
( not n <= b₁ or m <= f . b₁ )
let p be Element of A; :: thesis: ( not n <= p or m <= f . p )
assume A2: n <= p ; :: thesis: m <= f . p
thus m <= f . p by A2; :: thesis: verum

end;

then reconsider A = A as subnet of N ;
take A ; :: thesis: A is strict
thus A is strict ; :: thesis: verum