consider a being positive expression of C, an_Adj C;
take a ; :: thesis: a is regular
thus a is regular ; :: thesis: verum