Reloc (J,(card I)) is good by Th10;
hence I ";" J is good by Th12; :: thesis: verum