+
+theorem lfxs_trans_fsle: ∀R1,R2,R3.
+ lfxs_fsle_compatible R1 → lfxs_transitive_next R1 R2 R3 →
+ ∀L1,L,T. L1 ⪤*[R1, T] L →
+ ∀L2. L ⪤*[R2, T] L2 → L1 ⪤*[R3, T] L2.
+#R1 #R2 #R3 #H1R #H2R #L1 #L #T #H
+lapply (H1R … H) -H1R #H0
+cases H -H #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2
+lapply (fsle_inv_frees_eq … H0 … Hf1 … Hf2) -H0 -Hf2
+/4 width=14 by lexs_trans_gen, lexs_fwd_length, sle_lexs_trans, ex2_intro/
+qed-.