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

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