theorem :: ZFMISC_1:40

for x being object
for X being set st x in X holds
{x} \/ X = X by Lm1, XBOOLE_1:12;