consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type and
A2: the_arity_of m = {} and
the_result_sort_of a = an_Adj and
the_arity_of a = {} by Def12;
take m ; :: thesis: m is constructor
thus m <> * by A2, Def9; :: according to ABCMIZ_1:def 11 :: thesis: m <> non_op
thus m <> non_op by A1, Def9; :: thesis: verum