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 by A1, WAYBEL_0:def 32;
A3: ex_inf_of f " Y,L by 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:147
.= f . (inf (f " Y)) by A2, A3, WAYBEL_0:def 30 ;
then "/\" Y,M in rng f by FUNCT_2:6;
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