set W = if=0 (a,(I ';' (goto 0)));
card (if=0 (a,(I ';' (goto 0)))) = (card (I ';' (goto 0))) + 4 by Th1
.= ((card I) + 1) + 4 by COMPOS_2:11
.= (card I) + 5 ;
then (card I) + 3 < card (if=0 (a,(I ';' (goto 0)))) by XREAL_1:8;
then ((card I) + 2) + 1 < card (if=0 (a,(I ';' (goto 0)))) ;
hence ( while=0 (a,I) is halt-ending & while=0 (a,I) is unique-halt ) by Th21; :: thesis: verum