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 b1 being Element of the carrier of N ex b2 being Element of the carrier of A st
for b3 being Element of the carrier of A holds
( not b2 <= b3 or b1 <= f . b3 ) ) )
thus the mapping of A = the mapping of N * f by FUNCT_2:17; :: thesis: for b1 being Element of the carrier of N ex b2 being Element of the carrier of A st
for b3 being Element of the carrier of A holds
( not b2 <= b3 or b1 <= f . b3 )
let m be Element of N; :: thesis: ex b1 being Element of the carrier of A st
for b2 being Element of the carrier of A holds
( not b1 <= b2 or m <= f . b2 )
reconsider n = m as Element of A ;
take n ; :: thesis: for b1 being Element of the carrier of A holds
( not n <= b1 or m <= f . b1 )
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