let I be Program of SCMPDS ; :: thesis: inspos 0 in dom (stop I)
card (stop I) = (card I) + 1 by Th45, Th74;
hence inspos 0 in dom (stop I) by Th1; :: thesis: verum