:: deftheorem Def10 defines Net-Str WAYBEL11:def 10 :
for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R
for b₄ being non empty strict NetStr over R holds
( b₄ = Net-Str (S,f) iff ( the carrier of b₄ = S & the mapping of b₄ = f & ( for i, j being Element of b₄ holds
( i <= j iff b₄ . i <= b₄ . j ) ) ) );