theorem :: SCMPDS_6:125

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P ) ;