let I be Program of SCMPDS ; :: thesis: I c= Initialize (stop I)
set pI = stop I;
A1: I c= stop I by SCMPDS_4:40;
stop I c= Initialize (stop I) by SCMPDS_4:9;
hence I c= Initialize (stop I) by A1, XBOOLE_1:1; :: thesis: verum