Monotonicity of relation composition (source code)

= Monotonicity of relation composition

If $R\subseteq R'$ and $S\subseteq S'$, then $R\circ S\subseteq R'\circ S'$. A witness joining a pair through $S$ and then $R$ also joins it through the larger relations. If both $R$ and $S$ are <reflexive relations> on the same <set>, inserting an identity step gives $R\cup S\subseteq R\circ S$, so monotonicity also gives $(R\cup S)^2\subseteq(R\circ S)^2$.