consider m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that
A1: ( m is nullary & a is nullary ) by Th38;
take m ; :: thesis: ( m is nullary & m is constructor )
thus ( m is nullary & m is constructor ) by A1; :: thesis: verum