let I be Program of SCMPDS; :: thesis: I c= Initialize (stop I)
set pI = stop I;
A1: I c= stop I by AFINSQ_1:78;
stop I c= Initialize (stop I) by COMPOS_1:126;
hence I c= Initialize (stop I) by A1, XBOOLE_1:1; :: thesis: verum