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 )
( 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 infs-preserving )
thus f = g ; :: thesis: g is infs-preserving

now

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

now

assume A4: ex_inf_of X,L1 ; :: thesis: ( ex_inf_of g .: X,L3 & inf (g .: X) = g . (inf X) )
A5: f preserves_inf_of X by A1, WAYBEL_0:def 32;
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:64
.= g . (inf X) by A4, A5, 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