 The use of metavariables encompasses substitution (that we illustrated above on the term \(\textsf{W}MN)\).  The identity axiom and the rule of transitivity imply that \(\triangleright\) is a transitive and reflexive relation. The last two rules characterize application as an operation that is monotone in both of its argument places. \(\text{CL}_\triangleright\) includes only \(\textsf{S}\) and \(\textsf{K}\), because the other combinators are definable from them—as we already mentioned in section 1.2, and as we explain more precisely toward the end of this section.