This paper presents an approach for proving the validity of first-order relational formulas that involve transitive closure. Given a formula $F$ that includes the transitive closure of a relation $R$, our approach can deduce a complete (pure) first-order axiomatization of the paths of $R$ that occur in $F$. Such axiomatization enables full automated verification of $F$ using an automatic theorem prover like Z3. This is done via an iterative detection and injection of $R$-invariants ---invariant formulas with respect to $R$-transitions in the context of $F$. This paper presents a proof for the correctness of the approach, and reports on its application to non-trivial Alloy benchmarks.