let i be Instruction of SCMPDS; :: thesis: card (stop (Load i)) = 2
thus card (stop (Load i)) = (card (Load i)) + 1 by LL, AFINSQ_1:20
.= 1 + 1 by Th6
.= 2 ; :: thesis: verum