let I be Program of SCMPDS ; :: thesis: I c= Initialized (stop I)
set pI = stop I;
stop I = I ';' (Stop SCMPDS ) by SCMPDS_4:def 7;
then A1: I c= stop I by SCMPDS_4:40;
stop I c= Initialized (stop I) by SCMPDS_4:9;
hence I c= Initialized (stop I) by A1, XBOOLE_1:1; :: thesis: verum