let X be set ; :: thesis: for x being object holds
( x in succ X iff ( x in X or x = X ) )
let x be object ; :: thesis: ( x in succ X iff ( x in X or x = X ) )
thus ( not x in succ X or x in X or x = X ) :: thesis: ( ( x in X or x = X ) implies x in succ X )

proof

assume x in succ X ; :: thesis: ( x in X or x = X )
then ( x in X or x in {X} ) by XBOOLE_0:def 3;
hence ( x in X or x = X ) by TARSKI:def 1; :: thesis: verum

end;

assume ( x in X or x = X ) ; :: thesis: x in succ X
then ( x in X or x in {X} ) by TARSKI:def 1;
hence x in succ X by XBOOLE_0:def 3; :: thesis: verum