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