theorem lexs_trans (RN) (RP) (f): (∀g,I,K. lexs_transitive RN RN RN RN RP g K I) →
(∀g,I,K. lexs_transitive RP RP RP RN RP g K I) →
Transitive … (lexs RN RP f).
/2 width=9 by lexs_trans_gen/ qed-.
theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ →
theorem lexs_trans (RN) (RP) (f): (∀g,I,K. lexs_transitive RN RN RN RN RP g K I) →
(∀g,I,K. lexs_transitive RP RP RP RN RP g K I) →
Transitive … (lexs RN RP f).
/2 width=9 by lexs_trans_gen/ qed-.
theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ →