let X be set ; :: thesis: for c being Function of (),() st c is idempotent & c is directed-sups-preserving holds
inclusion c is directed-sups-preserving

let c be Function of (),(); :: thesis: ( c is idempotent & c is directed-sups-preserving implies inclusion c is directed-sups-preserving )
assume A1: ( c is idempotent & c is directed-sups-preserving ) ; :: thesis:
now :: thesis: for Y being Ideal of () holds inclusion c preserves_sup_of Y
let Y be Ideal of (); :: thesis:
now :: thesis: ( ex_sup_of Y, Image c implies ( ex_sup_of () .: Y, BoolePoset X & sup (() .: Y) = () . (sup Y) ) )
"\/" (Y,()) in the carrier of () ;
then "\/" (Y,()) in dom c by FUNCT_2:def 1;
then A2: c . ("\/" (Y,())) in rng c by FUNCT_1:def 3;
Y c= the carrier of () ;
then A3: Y c= rng c by YELLOW_0:def 15;
reconsider Y9 = Y as non empty directed Subset of () by YELLOW_2:7;
assume ex_sup_of Y, Image c ; :: thesis: ( ex_sup_of () .: Y, BoolePoset X & sup (() .: Y) = () . (sup Y) )
A4: ex_sup_of Y, BoolePoset X by YELLOW_0:17;
c preserves_sup_of Y9 by ;
then "\/" ((c .: Y),()) in rng c by ;
then "\/" (Y,()) in rng c by ;
then A5: "\/" (Y,()) in the carrier of () by YELLOW_0:def 15;
thus ex_sup_of () .: Y, BoolePoset X by YELLOW_0:17; :: thesis: sup (() .: Y) = () . (sup Y)
thus sup (() .: Y) = "\/" (Y,()) by FUNCT_1:92
.= sup Y by
.= () . (sup Y) ; :: thesis: verum
end;
hence inclusion c preserves_sup_of Y by WAYBEL_0:def 31; :: thesis: verum
end;
hence inclusion c is directed-sups-preserving by WAYBEL_0:73; :: thesis: verum