let L be complete LATTICE; :: thesis: for M being non empty RelStr
for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting
let M be non empty RelStr ; :: thesis: for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting
let f be Function of L,M; :: thesis: ( f is infs-preserving implies Image f is infs-inheriting )
assume A1: f is infs-preserving ; :: thesis: Image f is infs-inheriting
set S = subrelstr (rng f);
for Y being Subset of (subrelstr (rng f)) st ex_inf_of Y,M holds
"/\" (Y,M) in the carrier of (subrelstr (rng f))

proof

let Y be Subset of (subrelstr (rng f)); :: thesis: ( ex_inf_of Y,M implies "/\" (Y,M) in the carrier of (subrelstr (rng f)) )
assume ex_inf_of Y,M ; :: thesis: "/\" (Y,M) in the carrier of (subrelstr (rng f))
A2: ( f preserves_inf_of f " Y & ex_inf_of f " Y,L ) by A1, YELLOW_0:17;
Y c= the carrier of (subrelstr (rng f)) ;
then Y c= rng f by YELLOW_0:def 15;
then "/\" (Y,M) = inf (f .: (f " Y)) by FUNCT_1:77
.= f . (inf (f " Y)) by A2 ;
then "/\" (Y,M) in rng f by FUNCT_2:4;
hence "/\" (Y,M) in the carrier of (subrelstr (rng f)) by YELLOW_0:def 15; :: thesis: verum

end;

hence Image f is infs-inheriting by YELLOW_0:def 18; :: thesis: verum