let x be set ; :: thesis: (succ x) \ x = {x}
not x in x ;
then ( succ x = x \/ {x} & x nin x ) ;
hence (succ x) \ x = {x} by XBOOLE_1:88, ZFMISC_1:50; :: thesis: verum