let s be State of SCMPDS; :: thesis: for I, J being Program of SCMPDS holds
( I is_closed_on s iff I is_closed_on (Initialize s) +* J )
let I, J be Program of SCMPDS; :: thesis: ( I is_closed_on s iff I is_closed_on (Initialize s) +* J )
DataPart s = DataPart ((Initialize s) +* J) by Th9;
hence ( I is_closed_on s iff I is_closed_on (Initialize s) +* J ) by Th36; :: thesis: verum