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