theorem :: ZFMISC_1:129

for A, B being set st B in [:A,B:] holds
ex x being object st
( x in A & B = [x,{x}] )