set o = the constructor nullary OperSymbol of a_Type C;
take the constructor nullary OperSymbol of a_Type C ; :: thesis: ( the constructor nullary OperSymbol of a_Type C is nullary & the constructor nullary OperSymbol of a_Type C is constructor )
thus ( the constructor nullary OperSymbol of a_Type C is nullary & the constructor nullary OperSymbol of a_Type C is constructor ) ; :: thesis: verum