let S be COM-Struct ; :: thesis: (card (Stop S)) -' 1 = 0
thus (card (Stop S)) -' 1 = (card (Stop S)) - 1 by PRE_CIRC:20
.= 1 - 1 by AFINSQ_1:34
.= 0 ; :: thesis: verum