let X be set ; :: thesis: X /\ (succ X) = X
for x being object holds
( ( x in X & x in succ X ) iff x in X ) by XBOOLE_0:def 3;
hence X /\ (succ X) = X by XBOOLE_0:def 4; :: thesis: verum