- (â\88\80g,I,K,n. â¬\87*[n] L1 â\89\98 K.â\93\98{I} → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
- (â\88\80g,I,K,n. â¬\87*[n] L1 â\89\98 K.â\93\98{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.
+ (â\88\80g,I,K,n. â\87©*[n] L1 â\89\98 K.â\93\98[I] → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
+ (â\88\80g,I,K,n. â\87©*[n] L1 â\89\98 K.â\93\98[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.