theorem Th5: :: WAYBEL17:5

for S being non empty RelStr
for a, b being Element of S
for i being Element of (Net-Str (a,b)) holds
( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )