let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS holds
( I is_closed_on s iff I is_closed_on Initialize s )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s iff I is_closed_on Initialize s )
thus ( I is_closed_on s implies I is_closed_on Initialize s ) :: thesis: ( I is_closed_on Initialize s implies I is_closed_on s )

proof

assume for k being Element of NAT holds IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: I is_closed_on Initialize s
hence for k being Element of NAT holds IC (Comput ((ProgramPart ((Initialize (Initialize s)) +* (stop I))),((Initialize (Initialize s)) +* (stop I)),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: verum

end;

assume for k being Element of NAT holds IC (Comput ((ProgramPart ((Initialize (Initialize s)) +* (stop I))),((Initialize (Initialize s)) +* (stop I)),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: I is_closed_on s
hence for k being Element of NAT holds IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: verum