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