- ∀L1,f.
- (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
- (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → sex_transitive RP1 RP2 RP RN1 RP1 g K I) →
- ∀L0. L1 ⪤[RN1,RP1,f] L0 →
- ∀L2. L0 ⪤[RN2,RP2,f] L2 →
- L1 ⪤[RN,RP,f] L2.
+ ∀L1,f.
+ (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_transitive_sex RN1 RN2 RN RN1 RP1 g K I) →
+ (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_transitive_sex RP1 RP2 RP RN1 RP1 g K I) →
+ ∀L0. L1 ⪤[RN1,RP1,f] L0 →
+ ∀L2. L0 ⪤[RN2,RP2,f] L2 →
+ L1 ⪤[RN,RP,f] L2.