let I be Program of SCMPDS ; :: thesis: for x being set holds
( not x in dom (Initialized I) or x in dom I or x = IC SCMPDS )
let x be set ; :: thesis: ( not x in dom (Initialized I) or x in dom I or x = IC SCMPDS )
A1: dom (Initialized I) = (dom I) \/ {(IC SCMPDS )} by Th27;
assume x in dom (Initialized I) ; :: thesis: ( x in dom I or x = IC SCMPDS )
then ( x in dom I or x in {(IC SCMPDS )} ) by A1, XBOOLE_0:def 3;
hence ( x in dom I or x = IC SCMPDS ) by TARSKI:def 1; :: thesis: verum