let I, J be Program of SCMPDS ; :: thesis: I c= stop (I ';' J)
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46;
hence I c= stop (I ';' J) by SCMPDS_4:40; :: thesis: verum