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 Th46;
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, Def13;
then A4: subrelstr Lc is sups-inheriting by Th52;
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, Th45 ;
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:

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 X' = X as Subset of L by XBOOLE_1:1;
assume A12: ex_sup_of X,L ; :: thesis:
A13: sup X' is_>=_than p .: X'

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

end;

p preserves_sup_of X' by A10, WAYBEL_0:def 33;
then ( ex_sup_of p .: X,L & sup (p .: X') = p . (sup X') ) by A12, WAYBEL_0:def 31;
then sup X' >= p . (sup X') 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:

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, XBOOLE_1:1;
then A18: "\/" X,L in the carrier of (subrelstr Lk) by A8, A11, A17, YELLOW_0:def 19;
( subrelstr Lc is sups-inheriting & X c= the carrier of (subrelstr Lc) ) by A3, A9, A5, Th52, XBOOLE_1:1;
then "\/" X,L in the carrier of (subrelstr Lc) by A17, YELLOW_0:def 19;
hence "\/" X,L in the carrier of (Image p) by A6, A5, A8, A18, XBOOLE_0:def 4; :: thesis:

end;

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

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

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

end;

p preserves_sup_of X' by A19, WAYBEL_0:def 37;
then ( ex_sup_of p .: X,L & sup (p .: X') = p . (sup X') ) by A21, WAYBEL_0:def 31;
then sup X' >= p . (sup X') 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, WAYBEL_0:def 4;
X c= the carrier of (subrelstr Lc) by A9, A5, XBOOLE_1:1;
then "\/" X,L in the carrier of (subrelstr Lc) by A27, A4, YELLOW_0:def 19;
hence "\/" X,L in the carrier of (Image p) by A6, A5, A8, A28, XBOOLE_0:def 4; :: thesis: