consider a being expression of C, an_Adj C;
(non_op C) term a is compound ;
hence ex b₁ being expression of C st b₁ is compound ; :: thesis: verum