let I, J be Program of SCMPDS; :: thesis: I c= stop (I ';' J)
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30;
hence I c= stop (I ';' J) by AFINSQ_1:78; :: thesis: verum