theorem :: COMPOS_2:7

for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S holds (i ';' j) ';' k = i ';' (j ';' k) by COMPOS_1:29;