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 Th43;
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;
then A4: subrelstr Lk is infs-inheriting by Th50;
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 infs-preserving ; :: thesis:
thus A11: subrelstr Lc is infs-inheriting :: thesis:

proof

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

proof

let y be Element of L; :: according to LATTICE3:def 8 :: 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 Lc by A5, A14;
then A16: ex x9 being Element of L st
( x9 = x & x9 <= p . x9 ) by A2;
inf X9 is_<=_than X9 by A12, YELLOW_0:31;
then inf X9 <= x by A14;
hence inf X9 <= y by A15, A16, ORDERS_2:3; :: thesis:

end;

p preserves_inf_of X9 by A10;
then ( ex_inf_of p .: X,L & inf (p .: X9) = p . (inf X9) ) by A12;
then inf X9 <= p . (inf X9) 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:

proof

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;
then A18: "/\" (X,L) in the carrier of (subrelstr Lc) by A5, A11, A17;
( subrelstr Lk is infs-inheriting & X c= the carrier of (subrelstr Lk) ) by A3, A7, A8, Th50;
then "/\" (X,L) in the carrier of (subrelstr Lk) 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 filtered-infs-preserving ; :: thesis:
thus A20: subrelstr Lc is filtered-infs-inheriting :: thesis:

proof

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

proof

let y be Element of L; :: according to LATTICE3:def 8 :: 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 Lc by A5, A23;
then A25: ex x9 being Element of L st
( x9 = x & x9 <= p . x9 ) by A2;
inf X9 is_<=_than X9 by A21, YELLOW_0:31;
then inf X9 <= x by A23;
hence inf X9 <= y by A24, A25, ORDERS_2:3; :: thesis:

end;

p preserves_inf_of X9 by A19;
then ( ex_inf_of p .: X,L & inf (p .: X9) = p . (inf X9) ) by A21;
then inf X9 <= p . (inf X9) 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;
X c= the carrier of (subrelstr Lk) by A7, A8;
then "/\" (X,L) in the carrier of (subrelstr Lk) by A27, A4;
hence "/\" (X,L) in the carrier of (Image p) by A6, A5, A8, A28, XBOOLE_0:def 4; :: thesis: