let L be complete LATTICE; :: thesis: for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
( Image f is directed-sups-inheriting & Image f is complete LATTICE )
let f be Function of L,L; :: thesis: ( f is idempotent & f is directed-sups-preserving implies ( Image f is directed-sups-inheriting & Image f is complete LATTICE ) )
set S = subrelstr (rng f);
set a = the Element of L;
dom f = the carrier of L by FUNCT_2:def 1;
then f . the Element of L in rng f by FUNCT_1:def 3;
then reconsider S9 = subrelstr (rng f) as non empty full SubRelStr of L ;
assume A1: ( f is idempotent & f is directed-sups-preserving ) ; :: thesis: ( Image f is directed-sups-inheriting & Image f is complete LATTICE )
for X being directed Subset of (subrelstr (rng f)) st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of (subrelstr (rng f))

proof

let X be directed Subset of (subrelstr (rng f)); :: thesis: ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of (subrelstr (rng f)) )
X c= the carrier of (subrelstr (rng f)) ;
then A2: X c= rng f by YELLOW_0:def 15;
assume X <> {} ; :: thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr (rng f)) )
then X is non empty directed Subset of S9 ;
then reconsider X9 = X as non empty directed Subset of L by Th7;
assume A3: ex_sup_of X,L ; :: thesis: "\/" (X,L) in the carrier of (subrelstr (rng f))
f preserves_sup_of X9 by A1;
then sup (f .: X9) = f . (sup X9) by A3;
then sup X9 = f . (sup X9) by A1, A2, Th20;
then "\/" (X,L) in rng f by FUNCT_2:4;
hence "\/" (X,L) in the carrier of (subrelstr (rng f)) by YELLOW_0:def 15; :: thesis: verum

end;

hence Image f is directed-sups-inheriting ; :: thesis: Image f is complete LATTICE
rng f = { x where x is Element of L : x = f . x } by A1, Th19;
hence Image f is complete LATTICE by A1, Th16, Th29; :: thesis: verum