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