How to prove that a relation property holds for a transitive closure of this relation?

I defined the following relation property:

definition rel_limited_under :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
  "rel_limited_under R A = 
   (∀x y z :: 'a. R x y ⟶ R y z ⟶ x ∈ A ⟶ z ∈ A ⟶ y ∈ A)"

A relation R is limited under a set A iff any two elements x and z from this set can be related only through an element y belonging to this set. In other words elements from set A can't be related through an element not belonging to this set.

Do you know a common name of this property? I think it's something from graph theory.

Could you suggest how to prove that the property holds for transitive closure of a relation?

lemma rel_tcl_limited_under:
  fixes R :: "'a ⇒ 'a ⇒ bool"
    and A :: "'a set"
  assumes as_R: "rel_limited_under R A"
  shows "rel_limited_under R⇧+⇧+ A"

Solution

I can tell you that you cannot prove the property rel_tcl_limited_under in Isabelle, since it just does not hold. As a counterexample, consider A = {0} and R = {(0,1), (1,2), (2,0)}. Then rel_limited_under R A is trivially satisfied, since there are no x, y, z such that R x y /\ R y z /\ x ∈ A /\ z ∈ A. But rel_limited_under (R^+) A does not hold: choose x = 0, y = 1, z = 0.