(* Main properties **********************************************************)
theorem tc_lfxs_trans: ∀R,T. Transitive … (tc_lfxs R T).
(* Main properties **********************************************************)
theorem tc_lfxs_trans: ∀R,T. Transitive … (tc_lfxs R T).