In bisimulation as used in modal logic part of the structure is this:
Suppose there are sets $W_1, W_2$ each supporting a binary relation $R_i \subseteq W_i \times W_i$ for $i = 1,2$, and that $Z \subseteq W_1 \times W_2$. Then $Z$ is said to satisfy the forth condition provided $Z R_1^{-1} \subseteq R_2^{-1} Z$ and $Z$ is said to satisfy the back condition provided $R_2 Z \subseteq Z R_1 $.
I am interested in a weaker version of the forth condition:
Given any $(w_1, v_1) \in R_1$ such that there is some $(v_1, v_2) \in Z$, then for each $(w_1, w_2) \in Z$ there is some $u \in W_2$ such that $(v_1, u) \in Z$ and $(w_2,u) \in R_2$.
The following diagram shows elements $w_1, v_1, v_2, w_2, u$ and some pairs in the relations.
I am tempted to say "existential forth" or maybe "domain-restricted forth" in view of:
It is equivalent to defining a relation $D \subseteq W_1 \times W_1$ (the domain of $Z$) as the subrelation of the identity where $(w,w)\in D$ iff there is some $(w,v') \in Z$ and then asking that $$Z R_1^{-1} D \subseteq R_2^{-1} Z.$$
Question: Is this condition known anywhere? Does it have an accepted name?