let L1, L2, L3 be non empty transitive antisymmetric RelStr ; :: thesis: for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is infs-preserving )
let f be Function of L1,L2; :: thesis: ( f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete implies ex g being Function of L1,L3 st
( f = g & g is infs-preserving ) )
assume that
A1: f is infs-preserving and
A2: L2 is full infs-inheriting SubRelStr of L3 and
A3: L3 is complete ; :: thesis: ex g being Function of L1,L3 st
( f = g & g is infs-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 infs-preserving )
thus f = g ; :: thesis: g is infs-preserving

now :: thesis: for X being Subset of L1 holds g preserves_inf_of X

let X be Subset of L1; :: thesis: g preserves_inf_of X

now :: thesis: ( ex_inf_of X,L1 implies ( ex_inf_of g .: X,L3 & inf (g .: X) = g . (inf X) ) )

A4: f preserves_inf_of X by A1, WAYBEL_0:def 32;
assume A5: ex_inf_of X,L1 ; :: thesis: ( ex_inf_of g .: X,L3 & inf (g .: X) = g . (inf X) )
thus A6: ex_inf_of g .: X,L3 by A3, YELLOW_0:17; :: thesis: inf (g .: X) = g . (inf X)
then "/\" ((f .: X),L3) in the carrier of L2 by A2, YELLOW_0:def 18;
hence inf (g .: X) = inf (f .: X) by A2, A6, YELLOW_0:63
.= g . (inf X) by A5, A4, WAYBEL_0:def 30 ;
:: thesis: verum

end;

hence g preserves_inf_of X by WAYBEL_0:def 30; :: thesis: verum

end;

hence g is infs-preserving by WAYBEL_0:def 32; :: thesis: verum