let S be COM-Struct ; :: thesis: 0 in dom (Stop S)
dom (Stop S) = 1 by AFINSQ_1:33;
hence 0 in dom (Stop S) by CARD_1:49, TARSKI:def 1; :: thesis: verum