let S be COM-Struct ; :: thesis: 0 in dom (Stop S)
thus 0 in dom (Stop S) by TARSKI:def 1; :: thesis: verum