theorem :: ZFMISC_1:53

for x, y being object
for X being set holds
( not {x,y} /\ X = {x} or not y in X or x = y )