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

proof

let Y be Subset of (subrelstr (rng f)); :: thesis: ( ex_sup_of Y,M implies "\/" (Y,M) in the carrier of (subrelstr (rng f)) )
assume ex_sup_of Y,M ; :: thesis: "\/" (Y,M) in the carrier of (subrelstr (rng f))
A2: ( f preserves_sup_of f " Y & ex_sup_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) = sup (f .: (f " Y)) by FUNCT_1:77
.= f . (sup (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 sups-inheriting by YELLOW_0:def 19; :: thesis: verum