let L1, L2, L3 be non empty transitive antisymmetric RelStr ; 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; ( 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
; 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
; ( f = g & g is infs-preserving )
thus
f = g
; g is infs-preserving
now for X being Subset of L1 holds g preserves_inf_of Xlet X be
Subset of
L1;
g preserves_inf_of Xnow ( 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
;
( 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;
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
;
verum end; hence
g preserves_inf_of X
by WAYBEL_0:def 30;
verum end;
hence
g is infs-preserving
by WAYBEL_0:def 32; verum