let L1, L2, L3 be non empty transitive antisymmetric RelStr ; :: thesis: 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 )
let f be Function of L1,L2; :: thesis: ( f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving ) )
assume that
A1: ( f is monotone & f is directed-sups-preserving ) and
A2: L2 is full directed-sups-inheriting SubRelStr of L3 and
A3: L3 is complete ; :: thesis: ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving )
( not the carrier of L2 is empty & the carrier of L2 c= the carrier of L3 ) by A2, YELLOW_0:def 13;
then reconsider g = f as Function of L1,L3 by FUNCT_2:9;
take g ; :: thesis: ( f = g & g is directed-sups-preserving )
thus f = g ; :: thesis: g is directed-sups-preserving

now

let X be Subset of L1; :: thesis: ( not X is empty & X is directed implies g preserves_sup_of X )
assume A4: ( not X is empty & X is directed ) ; :: thesis: g preserves_sup_of X
then consider d being set such that
A5: d in X by XBOOLE_0:def 1;
( not the carrier of L2 is empty & d in the carrier of L1 ) by A5;
then d in dom f by FUNCT_2:def 1;
then f . d in f .: X by A5, FUNCT_1:def 12;
then A6: ( not f .: X is empty & f .: X is directed ) by A1, A4, YELLOW_2:17;

now

assume A7: ex_sup_of X,L1 ; :: thesis: ( ex_sup_of g .: X,L3 & sup (g .: X) = g . (sup X) )
A8: f preserves_sup_of X by A1, A4, WAYBEL_0:def 37;
thus ex_sup_of g .: X,L3 by A3, YELLOW_0:17; :: thesis: sup (g .: X) = g . (sup X)
hence sup (g .: X) = sup (f .: X) by A2, A6, WAYBEL_0:7
.= g . (sup X) by A7, A8, WAYBEL_0:def 31 ;
:: thesis: verum

end;

hence g preserves_sup_of X by WAYBEL_0:def 31; :: thesis: verum

end;

hence g is directed-sups-preserving by WAYBEL_0:def 37; :: thesis: verum