for L1, L2, L3 being non empty transitive antisymmetric RelStr
for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving )