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