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 :: thesis: for Y being Ideal of (Image c) holds inclusion c preserves_sup_of Y

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

now :: thesis: ( ex_sup_of Y, Image c implies ( ex_sup_of (inclusion c) .: Y, BoolePoset X & sup ((inclusion c) .: Y) = (inclusion c) . (sup Y) ) )

"\/" (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 3;
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:20;
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:92
.= sup Y by A4, A5, YELLOW_0:64
.= (inclusion c) . (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