:: deftheorem Def6 defines opp+id WAYBEL_9:def 6 :
for L being RelStr
for b₂ being strict NetStr over L holds
( b₂ = L opp+id iff ( the carrier of b₂ = the carrier of L & the InternalRel of b₂ = the InternalRel of L ~ & the mapping of b₂ = id L ) );