let I, J be Program of SCMPDS; :: thesis: I c= stop (I ';' J)
set IS = I ';' (J ';' (Stop SCMPDS));
set Ip = stop (I ';' J);
A2: I c= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:78;
thus I c= stop (I ';' J) by A2, AFINSQ_1:30; :: thesis: verum