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