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