let I be Program of ; :: thesis: card (stop (Directed I)) = card (stop I)
thus card (stop (Directed I)) = (card (Directed I)) + 1 by COMPOS_1:72
.= (card I) + 1 by Lm1
.= card (stop I) by COMPOS_1:72 ; :: thesis: verum