let o be OperSymbol of C; :: thesis: ( o is nullary implies o is constructor )
assume A1: the_arity_of o = {} ; :: according to ABCMIZ_A:def 13 :: thesis: o is constructor
( the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_arity_of (non_op C) = <*(an_Adj C)*> ) by ABCMIZ_1:38;
hence ( o <> * & o <> non_op ) by A1; :: according to ABCMIZ_1:def 11 :: thesis: verum