Description: Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012)