let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N holds card (Stop S) = 1
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of N; :: thesis: card (Stop S) = 1
thus card (Stop S) = card {[(il. S,0 ),(halt S)]} by FUNCT_4:87
.= 1 by CARD_1:50 ; :: thesis: verum