theorem Th9: :: WAYBEL17:9

for S being non empty reflexive RelStr
for D being non empty Subset of S holds Net-Str D = Net-Str (D,((id the carrier of S) | D))