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