let L be non empty reflexive transitive RelStr ; :: thesis: for D being non empty directed Subset of L
for n being Function of D,the carrier of L holds NetStr(# D,(the InternalRel of L |_2 D),n #) is net of L
let D be non empty directed Subset of L; :: thesis: for n being Function of D,the carrier of L holds NetStr(# D,(the InternalRel of L |_2 D),n #) is net of L
let n be Function of D,the carrier of L; :: thesis: NetStr(# D,(the InternalRel of L |_2 D),n #) is net of L
set N = NetStr(# D,(the InternalRel of L |_2 D),n #);
NetStr(# D,(the InternalRel of L |_2 D),n #) is SubRelStr of L

proof

thus the carrier of NetStr(# D,(the InternalRel of L |_2 D),n #) c= the carrier of L ; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of NetStr(# D,(the InternalRel of L |_2 D),n #) c= the InternalRel of L
thus the InternalRel of NetStr(# D,(the InternalRel of L |_2 D),n #) c= the InternalRel of L by XBOOLE_1:17; :: thesis: verum

end;

then reconsider N = NetStr(# D,(the InternalRel of L |_2 D),n #) as SubRelStr of L ;
N is full

proof

thus the InternalRel of N = the InternalRel of L |_2 the carrier of N ; :: according to YELLOW_0:def 14 :: thesis: verum

end;

then reconsider N = N as full SubRelStr of L ;
N is directed

proof

let x, y be Element of N; :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] N or not y in [#] N or ex b₁ being Element of the carrier of N st
( b₁ in [#] N & x <= b₁ & y <= b₁ ) )
assume ( x in [#] N & y in [#] N ) ; :: thesis: ex b₁ being Element of the carrier of N st
( b₁ in [#] N & x <= b₁ & y <= b₁ )
reconsider x1 = x, y1 = y as Element of D ;
consider z1 being Element of L such that
A1: ( z1 in D & x1 <= z1 & y1 <= z1 ) by WAYBEL_0:def 1;
reconsider z = z1 as Element of N by A1;
take z ; :: thesis: ( z in [#] N & x <= z & y <= z )
thus z in [#] N ; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A1, YELLOW_0:61; :: thesis: verum

end;

then reconsider N = N as prenet of L ;
N is transitive ;
hence NetStr(# D,(the InternalRel of L |_2 D),n #) is net of L ; :: thesis: verum