English
If r' is transitive and contains r, then every r-derivation is also an r'-derivation, provided r ⊆ r'.
Русский
Если r' является транзитивным и содержит r, то любая цепочка по r является цепочкой по r', если r ⊆ r'.
LaTeX
$$$$\\forall {α} {r r' : α \\to α \\to \\mathrm{Prop}}, \\mathrm{Transitive}\ r' \\to (\\forall x y, r x y \\to r' x y) \\\\to \\forall {x y}, \\operatorname{TransGen} r x y \\to r' x y$$$$
Lean4
theorem transGen_minimal {r' : α → α → Prop} (hr' : Transitive r') (h : ∀ x y, r x y → r' x y) {x y : α}
(hxy : TransGen r x y) : r' x y := by simpa [transGen_eq_self hr'] using TransGen.mono h hxy