let L be non empty 1-sorted ; :: thesis: for N being non empty transitive directed RelStr
for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L
let N be non empty transitive directed RelStr ; :: thesis: for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L
let f be Function of the carrier of N, the carrier of L; :: thesis: NetStr(# the carrier of N, the InternalRel of N,f #) is net of L
set N2 = NetStr(# the carrier of N, the InternalRel of N,f #);
A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) ;
[#] N is directed by WAYBEL_0:def 6;
then [#] NetStr(# the carrier of N, the InternalRel of N,f #) is directed by A1, WAYBEL_0:3;
hence NetStr(# the carrier of N, the InternalRel of N,f #) is net of L by A1, WAYBEL_0:def 6, WAYBEL_8:13; :: thesis: verum