:: deftheorem Def3 defines Net-Str WAYBEL17:def 3 :
for S being non empty RelStr
for a, b being Element of S
for b₄ being non empty strict NetStr over S holds
( b₄ = Net-Str (a,b) iff ( the carrier of b₄ = NAT & the mapping of b₄ = (a,b) ,... & ( for i, j being Element of b₄
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) ) );