let X be set ; :: thesis: (succ X) \ {X} = X
thus (succ X) \ {X} c= X :: according to XBOOLE_0:def 10 :: thesis: X c= (succ X) \ {X}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (succ X) \ {X} or x in X )
assume A1: x in (succ X) \ {X} ; :: thesis: x in X
then A2: not x in {X} by XBOOLE_0:def 5;
( x in X or x = X ) by A1, Th4;
hence x in X by A2, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (succ X) \ {X} )
assume A3: x in X ; :: thesis: x in (succ X) \ {X}
then reconsider xx = x as set ;
not xx in xx ;
then x <> X by A3;
then A4: not x in {X} by TARSKI:def 1;
x in succ X by A3, Th4;
hence x in (succ X) \ {X} by A4, XBOOLE_0:def 5; :: thesis: verum