theorem Th19: :: WAYBEL_2:19

for L being non empty reflexive RelStr
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