let L be complete LATTICE; :: thesis:
let f be Function of L,L; :: thesis:
assume A1: ( f is idempotent & f is directed-sups-preserving ) ; :: thesis:
set S = subrelstr (rng f);
consider a being Element of L;
dom f = the carrier of L by FUNCT_2:def 1;
then f . a in rng f by FUNCT_1:def 5;
then not the carrier of (subrelstr (rng f)) is empty ;
then reconsider S' = subrelstr (rng f) as non empty full SubRelStr of L ;
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))

let X be directed Subset of (subrelstr (rng f)); :: thesis:
assume X <> {} ; :: thesis:
then X is non empty directed Subset of S' ;
then reconsider X' = X as non empty directed Subset of L by Th7;
A2: f preserves_sup_of X' by A1, WAYBEL_0:def 37;
assume ex_sup_of X,L ; :: thesis:
then A3: ( ex_sup_of f .: X',L & sup (f .: X') = f . (sup X') ) by A2, WAYBEL_0:def 31;
X c= the carrier of (subrelstr (rng f)) ;
then X c= rng f by YELLOW_0:def 15;
then ( sup X' = f . (sup X') & the carrier of L <> {} ) by A1, A3, Th22;
then "\/" X,L in rng f by FUNCT_2:6;
hence "\/" X,L in the carrier of (subrelstr (rng f)) by YELLOW_0:def 15; :: thesis:

end;

hence Image f is directed-sups-inheriting by WAYBEL_0:def 4; :: thesis:
rng f = { x where x is Element of L : x = f . x } by A1, Th21;
hence Image f is complete LATTICE by A1, Th18, Th31; :: thesis: