for X being set holds X in succ X