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