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

hereby :: thesis:

assume A8: p is sups-preserving ; :: thesis:
thus A9: 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 A10: ex_sup_of X,L ; :: thesis:
p preserves_sup_of X' by A8, WAYBEL_0:def 33;
then A11: ( ex_sup_of p .: X,L & sup (p .: X') = p . (sup X') ) by A10, WAYBEL_0:def 31;
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
A12: x in X' and
A13: y = p . x by FUNCT_2:116;
reconsider x = x as Element of L ;
x in Lk by A6, A12;
then A14: ex x' being Element of L st
( x' = x & x' >= p . x' ) by A3;
sup X' is_>=_than X' by A10, YELLOW_0:30;
then sup X' >= x by A12, LATTICE3:def 9;
hence y <= sup X' by A13, A14, ORDERS_2:26; :: thesis:

end;

then sup X' >= p . (sup X') by A11, YELLOW_0:30;
hence "\/" X,L in the carrier of (subrelstr Lk) by A3, A6; :: thesis:

end;

thus Image p is sups-inheriting :: thesis:

let X be Subset of (Image p); :: according to YELLOW_0:def 19 :: thesis:
assume A15: ex_sup_of X,L ; :: thesis:
X c= Lk by A5, XBOOLE_1:1;
then A16: "\/" X,L in the carrier of (subrelstr Lk) by A6, A9, A15, YELLOW_0:def 19;
A17: subrelstr Lc is sups-inheriting by A2, Th52;
X c= the carrier of (subrelstr Lc) by A5, A6, XBOOLE_1:1;
then "\/" X,L in the carrier of (subrelstr Lc) by A15, A17, YELLOW_0:def 19;
hence "\/" X,L in the carrier of (Image p) by A4, A6, A16, XBOOLE_0:def 4; :: thesis:

end;

assume A18: p is directed-sups-preserving ; :: thesis:
thus A19: 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 A20: ex_sup_of X,L ; :: thesis:
p preserves_sup_of X' by A18, WAYBEL_0:def 37;
then A21: ( ex_sup_of p .: X,L & sup (p .: X') = p . (sup X') ) by A20, WAYBEL_0:def 31;
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
A22: x in X' and
A23: y = p . x by FUNCT_2:116;
reconsider x = x as Element of L ;
x in Lk by A6, A22;
then A24: ex x' being Element of L st
( x' = x & x' >= p . x' ) by A3;
sup X' is_>=_than X' by A20, YELLOW_0:30;
then sup X' >= x by A22, LATTICE3:def 9;
hence y <= sup X' by A23, A24, ORDERS_2:26; :: thesis:

end;

then sup X' >= p . (sup X') by A21, YELLOW_0:30;
hence "\/" X,L in the carrier of (subrelstr Lk) by A3, A6; :: thesis:

end;

let X be directed Subset of (Image p); :: according to WAYBEL_0:def 4 :: thesis:
assume that
A25: X <> {} and
A26: ex_sup_of X,L ; :: thesis:
X is directed Subset of (subrelstr Lk) by A7, YELLOW_2:8;
then A27: "\/" X,L in the carrier of (subrelstr Lk) by A19, A25, A26, WAYBEL_0:def 4;
A28: subrelstr Lc is sups-inheriting by A2, Th52;
X c= the carrier of (subrelstr Lc) by A5, A6, XBOOLE_1:1;
then "\/" X,L in the carrier of (subrelstr Lc) by A26, A28, YELLOW_0:def 19;
hence "\/" X,L in the carrier of (Image p) by A4, A6, A27, XBOOLE_0:def 4; :: thesis: