theorem :: SCMPDS_6:24

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