:: deftheorem Def7 defines | WAYBEL_9:def 7 :
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N
for b₄ being strict NetStr over L holds
( b₄ = N | i iff ( ( for x being object holds
( x in the carrier of b₄ iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b₄ = the InternalRel of N |_2 the carrier of b₄ & the mapping of b₄ = the mapping of N | the carrier of b₄ ) );