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