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

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

hence
inclusion c is directed-sups-preserving
by WAYBEL_0:73; :: thesis: verumlet Y be Ideal of (Image c); :: thesis: inclusion c preserves_sup_of Y

end;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) ) )

hence
inclusion c preserves_sup_of Y
by WAYBEL_0:def 31; :: thesis: verum
"\/" (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;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