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