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