let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite COM-Struct of N holds card (Stop S) = 1
let S be non empty stored-program IC-Ins-separated definite COM-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