Membership is checked in locks with the : operator, and
set by applying @EFFECTS to exits.
When checking for lack of membership the syntax should be:
!x:y implies something, not X, is a member of Y,
x:!y implies X is a member of something that isn't Y.
both are meaningless things to test for.
!(x:y) is the correct way to check if X is not a member of Y.