Description: A set belongs to its successor. This proof was automatically derived
from sucidALTVD using translate__without__overwriting.cmd and
minimizing. (Contributed by Alan Sare, 18-Feb-2012)(Proof modification is discouraged.)(New usage is discouraged.)