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 )
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:7;
take g ; :: thesis: ( f = g & g is directed-sups-preserving )
thus f = g ; :: thesis: g is directed-sups-preserving

now :: thesis: for X being Subset of L1 st not X is empty & X is directed holds
g preserves_sup_of X

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 object such that
A5: d in X by XBOOLE_0:def 1;
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 6;
then A6: ( not f .: X is empty & f .: X is directed ) by A1, A4, YELLOW_2:15;

now :: thesis: ( ex_sup_of X,L1 implies ( ex_sup_of g .: X,L3 & sup (g .: X) = g . (sup X) ) )

A7: f preserves_sup_of X by A1, A4, WAYBEL_0:def 37;
assume A8: ex_sup_of X,L1 ; :: thesis: ( ex_sup_of g .: X,L3 & sup (g .: X) = g . (sup X) )
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 A8, A7, 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