A1: Reloc (J,(card I)) is good by Th3;
I ";" J = (CutLastLoc (stop (Directed I))) +* (Reloc (J,((card (stop I)) -' 1))) by SCMFSA6A:37
.= (Directed I) +* (Reloc (J,(card I))) by COMPOS_1:71 ;
hence I ";" J is good by A1, Th5; :: thesis: verum