for X being ConstructorDB
for x, y being Element of X holds
( x in y ref iff y in x occur )