:: deftheorem Def3 defines "/\" WAYBEL_2:def 3 :
for L being non empty RelStr
for x being Element of L
for N being non empty NetStr over L
for b₄ being strict NetStr over L holds
( b₄ = x "/\" N iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b₄ ex y being Element of L st
( y = the mapping of N . i & the mapping of b₄ . i = x "/\" y ) ) ) );