theorem :: ZFMISC_1:128

for x being object
for B being set st B = [x,{x}] holds
B in [:{x},B:]