let i be Instruction of SCMPDS ; :: thesis: dom (stop (Load i)) = {(inspos 0 ),(inspos 1)}
for x being set holds
( x in dom (stop (Load i)) iff ( x = inspos 0 or x = inspos 1 ) ) by Th11;
hence dom (stop (Load i)) = {(inspos 0 ),(inspos 1)} by TARSKI:def 2; :: thesis: verum