let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite COM-Struct of N holds 0 in dom (Stop S)
let S be non empty stored-program definite COM-Struct of N; :: thesis: 0 in dom (Stop S)
dom (Stop S) = 1 by AFINSQ_1:36;
hence 0 in dom (Stop S) by CARD_1:87, TARSKI:def 1; :: thesis: verum