given m, a being OperSymbol of MinConstrSign such that the_result_sort_of m = a_Type and
A1: the_arity_of m = {} and
the_result_sort_of a = an_Adj and
the_arity_of a = {} ; :: according to ABCMIZ_1:def 12 :: thesis: contradiction
the carrier' of MinConstrSign = {*,non_op} by Def10;
then ( m = * or m = non_op ) by TARSKI:def 2;
hence contradiction by A1, Def9; :: thesis: verum