:: deftheorem Def5 defines +id WAYBEL_9:def 5 :
for L being RelStr
for b₂ being strict NetStr over L holds
( b₂ = L +id iff ( RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b₂ = id L ) );