for X being set holds X c= succ X by XBOOLE_1:7;