consider o being constructor nullary OperSymbol of a_Type C;
take o ; :: thesis: ( o is nullary & o is constructor )
thus ( o is nullary & o is constructor ) ; :: thesis: verum