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 ThInit;
take a ; :: thesis: ( a is nullary & a is constructor )
thus ( a is nullary & a is constructor ) by A1; :: thesis: verum