theorem :: ZFMISC_1:137

for x being object
for Y, X being set holds
( X \/ {x} c= Y iff ( x in Y & X c= Y ) )