for X being set holds X <> succ X