theorem :: SCMPDS_4:16

for i, j being Instruction of SCMPDS
for K being Program of holds (i ';' j) ';' K = i ';' (j ';' K) by AFINSQ_1:27;