let L be complete continuous LATTICE; :: thesis: for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )
let p be projection Function of L,L; :: thesis: ( p is infs-preserving implies ( Image p is continuous LATTICE & Image p is infs-inheriting ) )
assume A1: p is infs-preserving ; :: thesis: ( Image p is continuous LATTICE & Image p is infs-inheriting )
reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by WAYBEL_1:43;
reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by WAYBEL_1:45;
A2: subrelstr Lc is infs-inheriting by A1, WAYBEL_1:51;
then A3: subrelstr Lc is complete by YELLOW_2:30;
A4: pc is infs-preserving

proof

let X be Subset of (subrelstr Lc); :: according to WAYBEL_0:def 32 :: thesis: pc preserves_inf_of X
assume ex_inf_of X, subrelstr Lc ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of pc .: X, subrelstr Lc & "/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc))) )
thus ex_inf_of pc .: X, subrelstr Lc by A3, YELLOW_0:17; :: thesis: "/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc)))
the carrier of (subrelstr Lc) = Lc by YELLOW_0:def 15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
A5: ( ex_inf_of X9,L & p preserves_inf_of X9 ) by A1, YELLOW_0:17;
X c= the carrier of (subrelstr Lc) ;
then X c= Lc by YELLOW_0:def 15;
then A6: pc .: X = p .: X by RELAT_1:129;
A7: ex_inf_of X,L by YELLOW_0:17;
then "/\" (X9,L) in the carrier of (subrelstr Lc) by A2;
then A8: ( dom pc = the carrier of (subrelstr Lc) & inf X9 = inf X ) by A7, FUNCT_2:def 1, YELLOW_0:63;
( ex_inf_of p .: X,L & "/\" ((pc .: X),L) in the carrier of (subrelstr Lc) ) by A2, YELLOW_0:17;
hence inf (pc .: X) = inf (p .: X) by A6, YELLOW_0:63
.= p . (inf X9) by A5
.= pc . (inf X) by A8, FUNCT_1:47 ;
:: thesis: verum

end;

reconsider cpc = corestr pc as Function of (subrelstr Lc),(Image pc) ;
A9: the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def 15
.= rng pc by WAYBEL_1:44
.= the carrier of (subrelstr (rng pc)) by YELLOW_0:def 15 ;
subrelstr (rng pc) is full SubRelStr of L by WAYBEL15:1;
then A10: Image p = Image pc by A9, YELLOW_0:57;
pc is closure by WAYBEL_1:47;
then A11: cpc is sups-preserving by WAYBEL_1:55;
subrelstr Lc is sups-inheriting SubRelStr of L by WAYBEL_1:49;
then subrelstr Lc is continuous LATTICE by A2, WAYBEL_5:28;
hence Image p is continuous LATTICE by A3, A10, A4, A11, Th19, WAYBEL_5:33; :: thesis: Image p is infs-inheriting
thus Image p is infs-inheriting by A1, A2, WAYBEL_1:51; :: thesis: verum