Suppose we are given the following binary relations on a set $A$:
$$S \triangleleft R = \{(x,y) \mid \forall z\,(R(y,z) \to S(x,z)\,) \} $$ $$S \circ R = \{(x,y) \mid \exists z\,(R(x,z) \land S(z,y)\,) \} $$
and need to prove
$$(R \triangleleft T) \circ (S \triangleleft R) \subseteq (S \triangleleft T) $$
I think this cannot be proven. Suppose that $(x,y) \in (R \triangleleft T) \circ (S \triangleleft R)$ and $(x,y) \not\in (S \triangleleft T)$.
Decomposing the relations we end up with the question of whether the following formula of predicate logic is consistent:
$$\exists z \,(\forall z' (S(z,z') \to R(x,z')) \land \forall z''(R(y, z'') \to T(z, z'')\,) \land \neg (\forall z(S(y,z) \to T(x,z)\,)\,)\, ) $$
If it is inconsistent then $(x,y) \in S \triangleleft T$. However, I can't prove the formula inconsistent. I'm therefore wondering if
$$(R \triangleleft T) \circ (S \triangleleft R) \subseteq (S \triangleleft T) $$
is not in fact provable. I would appreciate any help with this.
Suppose that $(x,y) \in (R \triangleleft T) \circ (S \triangleleft R).$ Then there exists $z$ such that $(x,z) \in S \triangleleft R$ and $(z,y) \in R \triangleleft T,$ i.e. for all $w$ we have $R(y,w)\rightarrow S(x,w)$ and $T(y,w)\rightarrow R(z,w).$ Combining these, for all $w$ we have $T(y,w)\rightarrow S(x,w),$ i.e. $(x,y) \in S\triangleleft T.$ Thus, $(R \triangleleft T) \circ (S \triangleleft R) \subseteq S\triangleleft T.$