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 Lc be non empty Subset of L; :: thesis:
assume A3: Lc = { c where c is Element of L : c <= p . c } ; :: thesis:
reconsider Lk = { k where k is Element of L : p . k <= k } 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 Lc) by A5, YELLOW_0:def 15;

hereby :: thesis:

assume A8: p is infs-preserving ; :: thesis:
thus A9: subrelstr Lc is infs-inheriting :: thesis:

let X be Subset of (subrelstr Lc); :: according to YELLOW_0:def 18 :: thesis:
the carrier of (subrelstr Lc) is Subset of L by YELLOW_0:def 15;
then reconsider X' = X as Subset of L by XBOOLE_1:1;
assume A10: ex_inf_of X,L ; :: thesis:
p preserves_inf_of X' by A8, WAYBEL_0:def 32;
then A11: ( ex_inf_of p .: X,L & inf (p .: X') = p . (inf X') ) by A10, WAYBEL_0:def 30;
inf X' is_<=_than p .: X'

let y be Element of L; :: according to LATTICE3:def 8 :: 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 Lc by A6, A12;
then A14: ex x' being Element of L st
( x' = x & x' <= p . x' ) by A3;
inf X' is_<=_than X' by A10, YELLOW_0:31;
then inf X' <= x by A12, LATTICE3:def 8;
hence inf X' <= y by A13, A14, ORDERS_2:26; :: thesis:

end;

then inf X' <= p . (inf X') by A11, YELLOW_0:31;
hence "/\" X,L in the carrier of (subrelstr Lc) by A3, A6; :: thesis:

end;

thus Image p is infs-inheriting :: thesis:

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

end;

assume A18: p is filtered-infs-preserving ; :: thesis:
thus A19: subrelstr Lc is filtered-infs-inheriting :: thesis:

let X be filtered Subset of (subrelstr Lc); :: according to WAYBEL_0:def 3 :: thesis:
assume X <> {} ; :: thesis:
then reconsider X' = X as non empty filtered Subset of L by YELLOW_2:7;
assume A20: ex_inf_of X,L ; :: thesis:
p preserves_inf_of X' by A18, WAYBEL_0:def 36;
then A21: ( ex_inf_of p .: X,L & inf (p .: X') = p . (inf X') ) by A20, WAYBEL_0:def 30;
inf X' is_<=_than p .: X'

let y be Element of L; :: according to LATTICE3:def 8 :: 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 Lc by A6, A22;
then A24: ex x' being Element of L st
( x' = x & x' <= p . x' ) by A3;
inf X' is_<=_than X' by A20, YELLOW_0:31;
then inf X' <= x by A22, LATTICE3:def 8;
hence inf X' <= y by A23, A24, ORDERS_2:26; :: thesis:

end;

then inf X' <= p . (inf X') by A21, YELLOW_0:31;
hence "/\" X,L in the carrier of (subrelstr Lc) by A3, A6; :: thesis:

end;

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