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