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