∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1
[ #f1 #_ #L2 #H #f2 #_
lapply (sex_inv_atom1 … H) -H #H destruct
/2 width=3 by sex_atom, ex2_intro/
∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1
[ #f1 #_ #L2 #H #f2 #_
lapply (sex_inv_atom1 … H) -H #H destruct
/2 width=3 by sex_atom, ex2_intro/