let L be non empty Poset; :: thesis:
let p be Function of L,L; :: thesis:
assume A1: p is projection ; :: thesis:
then reconsider Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by Th46;
let Lc be non empty Subset of L; :: thesis:
assume A2: Lc = { c where c is Element of L : c <= p . c } ; :: thesis:
A3: p is monotone by A1, Def13;
then A4: subrelstr Lk is infs-inheriting by Th53;
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 infs-preserving ; :: thesis:
thus A11: 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 A12: ex_inf_of X,L ; :: thesis:
A13: 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
A14: x in X' and
A15: y = p . x by FUNCT_2:116;
reconsider x = x as Element of L ;
x in Lc by A5, A14;
then A16: ex x' being Element of L st
( x' = x & x' <= p . x' ) by A2;
inf X' is_<=_than X' by A12, YELLOW_0:31;
then inf X' <= x by A14, LATTICE3:def 8;
hence inf X' <= y by A15, A16, ORDERS_2:26; :: thesis:

end;

p preserves_inf_of X' by A10, WAYBEL_0:def 32;
then ( ex_inf_of p .: X,L & inf (p .: X') = p . (inf X') ) by A12, WAYBEL_0:def 30;
then inf X' <= p . (inf X') by A13, YELLOW_0:31;
hence "/\" X,L in the carrier of (subrelstr Lc) by A2, A5; :: thesis:

end;

thus Image p is infs-inheriting :: thesis:

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

end;

assume A19: p is filtered-infs-preserving ; :: thesis:
thus A20: 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 A21: ex_inf_of X,L ; :: thesis:
A22: 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
A23: x in X' and
A24: y = p . x by FUNCT_2:116;
reconsider x = x as Element of L ;
x in Lc by A5, A23;
then A25: ex x' being Element of L st
( x' = x & x' <= p . x' ) by A2;
inf X' is_<=_than X' by A21, YELLOW_0:31;
then inf X' <= x by A23, LATTICE3:def 8;
hence inf X' <= y by A24, A25, ORDERS_2:26; :: thesis:

end;

p preserves_inf_of X' by A19, WAYBEL_0:def 36;
then ( ex_inf_of p .: X,L & inf (p .: X') = p . (inf X') ) by A21, WAYBEL_0:def 30;
then inf X' <= p . (inf X') by A22, YELLOW_0:31;
hence "/\" X,L in the carrier of (subrelstr Lc) by A2, A5; :: thesis:

end;

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