let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting definite AMI-Struct of N holds card (Stop S) = 1
let S be non empty stored-program halting definite AMI-Struct of N; :: thesis: card (Stop S) = 1
thus card (Stop S) = card (dom (Stop S)) by CARD_1:104
.= dom (Stop S) by CARD_1:def 5
.= 1 by AFINSQ_1:36 ; :: thesis: verum