let L be non empty up-complete Poset; :: thesis: for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
Image f is directed-sups-inheriting
let f be Function of L,L; :: thesis: ( f is idempotent & f is directed-sups-preserving implies Image f is directed-sups-inheriting )
set S = subrelstr (rng f);
consider a being Element of ;
dom f = the carrier of L by FUNCT_2:def 1;
then f . a in rng f by FUNCT_1:def 5;
then reconsider S' = 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
subrelstr (rng f) is directed-sups-inheriting

proof

let X be directed Subset of ; :: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X,L or "\/" 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 ;
then reconsider X' = X as non empty directed Subset of by YELLOW_2:7;
assume A3: ex_sup_of X,L ; :: thesis: "\/" X,L in the carrier of (subrelstr (rng f))
f preserves_sup_of X' by A1, WAYBEL_0:def 37;
then sup (f .: X') = f . (sup X') by A3, WAYBEL_0:def 31;
then sup X' = f . (sup X') by A1, A2, YELLOW_2:22;
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: verum

end;

hence Image f is directed-sups-inheriting ; :: thesis: verum