let S be COM-Struct ; :: thesis: for I being Program of S holds card (stop I) = (card I) + 1
let I be Program of S; :: thesis: card (stop I) = (card I) + 1
thus card (stop I) = (card I) + (card (Stop S)) by AFINSQ_1:17
.= (card I) + 1 by AFINSQ_1:34 ; :: thesis: verum