theorem :: ZFMISC_1:34

for x being object
for X, Y being set st Y c= X & not x in Y holds
Y c= X \ {x} by Lm2;