set a = the positive expression of C, an_Adj C;
take the positive expression of C, an_Adj C ; :: thesis: the positive expression of C, an_Adj C is regular
thus the positive expression of C, an_Adj C is regular ; :: thesis: verum