let i be Instruction of SCMPDS; :: thesis: ( 0 in dom (stop (Load i)) & 1 in dom (stop (Load i)) )
card (stop (Load i)) = 2 by Th8;
hence ( 0 in dom (stop (Load i)) & 1 in dom (stop (Load i)) ) by AFINSQ_1:70; :: thesis: verum