theorem :: ZFMISC_1:38

for z being object
for X, Y being set st {z} = X \/ Y & X <> Y & not X = {} holds
Y = {}