let L be non empty reflexive 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 prenet 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 prenet of L
let n be Function of D, the carrier of L; :: thesis: NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L
set N = NetStr(# D,( the InternalRel of L |_2 D),n #);
NetStr(# D,( the InternalRel of L |_2 D),n #) is directed
proof
let x, y be Element of NetStr(# D,( the InternalRel of L |_2 D),n #); :: according to WAYBEL_0:def 1,WAYBEL_0:def 6 :: thesis: ( not x in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) or not y in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) or ex b1 being Element of the carrier of NetStr(# D,( the InternalRel of L |_2 D),n #) st
( b1 in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 ) )

assume that
x in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) and
y in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) ; :: thesis: ex b1 being Element of the carrier of NetStr(# D,( the InternalRel of L |_2 D),n #) st
( b1 in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 )

reconsider x1 = x, y1 = y as Element of D ;
consider z1 being Element of L such that
A1: z1 in D and
A2: ( x1 <= z1 & y1 <= z1 ) by WAYBEL_0:def 1;
reconsider z = z1 as Element of NetStr(# D,( the InternalRel of L |_2 D),n #) by A1;
take z ; :: thesis: ( z in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= z & y <= z )
thus z in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) ; :: thesis: ( x <= z & y <= z )
the InternalRel of NetStr(# D,( the InternalRel of L |_2 D),n #) c= the InternalRel of L by XBOOLE_1:17;
then reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as SubRelStr of L by YELLOW_0:def 13;
N is full ;
hence ( x <= z & y <= z ) by ; :: thesis: verum
end;
hence NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L ; :: thesis: verum