∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r₁₂ : α → β → Prop} {r₂₃ : β → γ → Prop} {r₁₃ : α → γ → Prop},
  (∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) →
    Relator.RightTotal r₁₂ → Relator.RightTotal r₂₃ → Relator.RightTotal r₁₃