let L be non empty Poset; :: thesis:
let p be Function of L,L; :: thesis:
assume A1: p is projection ; :: thesis:
then reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by Th43;
let Lk be non empty Subset of L; :: thesis:
assume A2: Lk = { k where k is Element of L : p . k <= k } ; :: thesis:
A3: p is monotone by A1;
then A4: subrelstr Lc is sups-inheriting by Th49;
A5: Lc = the carrier of (subrelstr Lc) by YELLOW_0:def 15;
A6: the carrier of (Image p) = rng p by YELLOW_0:def 15
.= Lc /\ Lk by A1, A2, Th42 ;
then A7: the carrier of (Image p) c= Lk by XBOOLE_1:17;
A8: Lk = the carrier of (subrelstr Lk) by YELLOW_0:def 15;
A9: the carrier of (Image p) c= Lc by A6, XBOOLE_1:17;

hereby :: thesis:

assume A10: p is sups-preserving ; :: thesis:
thus A11: subrelstr Lk is sups-inheriting :: thesis:

proof

let X be Subset of (subrelstr Lk); :: according to YELLOW_0:def 19 :: thesis:
the carrier of (subrelstr Lk) is Subset of L by YELLOW_0:def 15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume A12: ex_sup_of X,L ; :: thesis:
A13: sup X9 is_>=_than p .: X9

proof

let y be Element of L; :: according to LATTICE3:def 9 :: thesis:
assume y in p .: X9 ; :: thesis:
then consider x being Element of L such that
A14: x in X9 and
A15: y = p . x by FUNCT_2:65;
reconsider x = x as Element of L ;
x in Lk by A8, A14;
then A16: ex x9 being Element of L st
( x9 = x & x9 >= p . x9 ) by A2;
sup X9 is_>=_than X9 by A12, YELLOW_0:30;
then sup X9 >= x by A14;
hence y <= sup X9 by A15, A16, ORDERS_2:3; :: thesis:

end;

p preserves_sup_of X9 by A10;
then ( ex_sup_of p .: X,L & sup (p .: X9) = p . (sup X9) ) by A12;
then sup X9 >= p . (sup X9) by A13, YELLOW_0:30;
hence "\/" (X,L) in the carrier of (subrelstr Lk) by A2, A8; :: thesis:

end;

thus Image p is sups-inheriting :: thesis:

proof

let X be Subset of (Image p); :: according to YELLOW_0:def 19 :: thesis:
assume A17: ex_sup_of X,L ; :: thesis:
X c= Lk by A7;
then A18: "\/" (X,L) in the carrier of (subrelstr Lk) by A8, A11, A17;
( subrelstr Lc is sups-inheriting & X c= the carrier of (subrelstr Lc) ) by A3, A9, A5, Th49;
then "\/" (X,L) in the carrier of (subrelstr Lc) by A17;
hence "\/" (X,L) in the carrier of (Image p) by A6, A5, A8, A18, XBOOLE_0:def 4; :: thesis:

end;

end;

assume A19: p is directed-sups-preserving ; :: thesis:
thus A20: subrelstr Lk is directed-sups-inheriting :: thesis:

proof

let X be directed Subset of (subrelstr Lk); :: according to WAYBEL_0:def 4 :: thesis:
assume X <> {} ; :: thesis:
then reconsider X9 = X as non empty directed Subset of L by YELLOW_2:7;
assume A21: ex_sup_of X,L ; :: thesis:
A22: sup X9 is_>=_than p .: X9

proof

let y be Element of L; :: according to LATTICE3:def 9 :: thesis:
assume y in p .: X9 ; :: thesis:
then consider x being Element of L such that
A23: x in X9 and
A24: y = p . x by FUNCT_2:65;
reconsider x = x as Element of L ;
x in Lk by A8, A23;
then A25: ex x9 being Element of L st
( x9 = x & x9 >= p . x9 ) by A2;
sup X9 is_>=_than X9 by A21, YELLOW_0:30;
then sup X9 >= x by A23;
hence y <= sup X9 by A24, A25, ORDERS_2:3; :: thesis:

end;

p preserves_sup_of X9 by A19;
then ( ex_sup_of p .: X,L & sup (p .: X9) = p . (sup X9) ) by A21;
then sup X9 >= p . (sup X9) by A22, YELLOW_0:30;
hence "\/" (X,L) in the carrier of (subrelstr Lk) by A2, A8; :: thesis:

end;

let X be directed Subset of (Image p); :: according to WAYBEL_0:def 4 :: thesis:
assume that
A26: X <> {} and
A27: ex_sup_of X,L ; :: thesis:
the carrier of (Image p) c= the carrier of (subrelstr Lk) by A7, YELLOW_0:def 15;
then X is directed Subset of (subrelstr Lk) by YELLOW_2:8;
then A28: "\/" (X,L) in the carrier of (subrelstr Lk) by A20, A26, A27;
X c= the carrier of (subrelstr Lc) by A9, A5;
then "\/" (X,L) in the carrier of (subrelstr Lc) by A27, A4;
hence "\/" (X,L) in the carrier of (Image p) by A6, A5, A8, A28, XBOOLE_0:def 4; :: thesis: