theorem :: ZFMISC_1:138

for a being object
for A, B being set st A c= B & B c= A \/ {a} & not A \/ {a} = B holds
A = B