let X be set ; :: thesis: for c being Function of (BoolePoset X),(BoolePoset X) st c is idempotent & c is directed-sups-preserving holds
inclusion c is directed-sups-preserving
let c be Function of (BoolePoset X),(BoolePoset X); :: 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: inclusion c is directed-sups-preserving

now

let Y be Ideal of (Image c); :: thesis: inclusion c preserves_sup_of Y

now

"\/" Y,(BoolePoset X) in the carrier of (BoolePoset X) ;
then "\/" Y,(BoolePoset X) in dom c by FUNCT_2:def 1;
then A2: c . ("\/" Y,(BoolePoset X)) in rng c by FUNCT_1:def 5;
Y c= the carrier of (Image c) ;
then A3: Y c= rng c by YELLOW_0:def 15;
reconsider Y9 = Y as non empty directed Subset of (BoolePoset X) by YELLOW_2:7;
assume ex_sup_of Y, Image c ; :: thesis: ( ex_sup_of (inclusion c) .: Y, BoolePoset X & sup ((inclusion c) .: Y) = (inclusion c) . (sup Y) )
A4: ex_sup_of Y, BoolePoset X by YELLOW_0:17;
c preserves_sup_of Y9 by A1, WAYBEL_0:def 37;
then "\/" (c .: Y),(BoolePoset X) in rng c by A4, A2, WAYBEL_0:def 31;
then "\/" Y,(BoolePoset X) in rng c by A1, A3, YELLOW_2:22;
then A5: "\/" Y,(BoolePoset X) in the carrier of (Image c) by YELLOW_0:def 15;
thus ex_sup_of (inclusion c) .: Y, BoolePoset X by YELLOW_0:17; :: thesis: sup ((inclusion c) .: Y) = (inclusion c) . (sup Y)
thus sup ((inclusion c) .: Y) = "\/" Y,(BoolePoset X) by FUNCT_1:162
.= sup Y by A4, A5, YELLOW_0:65
.= (inclusion c) . (sup Y) by TMAP_1:91 ; :: 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