set a = the positive expression of C, an_Adj C;
take Non the positive expression of C, an_Adj C ; :: thesis: ( Non the positive expression of C, an_Adj C is negative & not Non the positive expression of C, an_Adj C is positive )
thus ( Non the positive expression of C, an_Adj C is negative & not Non the positive expression of C, an_Adj C is positive ) ; :: thesis: verum