ProgramPart (Relocated (J,(card I))) is good by Th24;
hence I ';' J is good by Th26; :: thesis: verum