theorem Th6: :: WAYBEL17:6

for S being non empty RelStr
for a, b being Element of S
for i, j being Element of (Net-Str (a,b))
for i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds
( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )