let L be complete continuous LATTICE; :: thesis: for p being projection Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
let p be projection Function of L,L; :: thesis: ( p is directed-sups-preserving implies Image p is continuous LATTICE )
assume A1: p is directed-sups-preserving ; :: thesis: Image p is continuous LATTICE
reconsider Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by WAYBEL_1:43;
A2: subrelstr Lk is infs-inheriting by WAYBEL_1:50;
reconsider pk = p | Lk as Function of (subrelstr Lk),(subrelstr Lk) by WAYBEL_1:46;
A3: pk is kernel by WAYBEL_1:48;

now :: thesis: for X being Subset of (subrelstr Lk) st not X is empty & X is directed holds
pk preserves_sup_of X

let X be Subset of (subrelstr Lk); :: thesis: ( not X is empty & X is directed implies pk preserves_sup_of X )
reconsider X9 = X as Subset of L by WAYBEL13:3;
assume A4: ( not X is empty & X is directed ) ; :: thesis: pk preserves_sup_of X
then reconsider X9 = X9 as non empty directed Subset of L by YELLOW_2:7;
A5: p preserves_sup_of X9 by A1, WAYBEL_0:def 37;

now :: thesis: ( ex_sup_of X, subrelstr Lk implies ( ex_sup_of pk .: X, subrelstr Lk & sup (pk .: X) = pk . (sup X) ) )

X c= the carrier of (subrelstr Lk) ;
then X c= Lk by YELLOW_0:def 15;
then A6: pk .: X = p .: X by RELAT_1:129;
assume ex_sup_of X, subrelstr Lk ; :: thesis: ( ex_sup_of pk .: X, subrelstr Lk & sup (pk .: X) = pk . (sup X) )
subrelstr Lk is infs-inheriting by WAYBEL_1:50;
then subrelstr Lk is complete LATTICE by YELLOW_2:30;
hence ex_sup_of pk .: X, subrelstr Lk by YELLOW_0:17; :: thesis: sup (pk .: X) = pk . (sup X)
A7: ex_sup_of X,L by YELLOW_0:17;
A8: subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;
then A9: ( dom pk = the carrier of (subrelstr Lk) & sup X9 = sup X ) by A4, A7, FUNCT_2:def 1, WAYBEL_0:7;
( ex_sup_of p .: X,L & pk .: X is directed Subset of (subrelstr Lk) ) by A3, A4, YELLOW_0:17, YELLOW_2:15;
hence sup (pk .: X) = sup (p .: X) by A4, A8, A6, WAYBEL_0:7
.= p . (sup X9) by A5, A7, WAYBEL_0:def 31
.= pk . (sup X) by A9, FUNCT_1:47 ;
:: thesis: verum

end;

hence pk preserves_sup_of X by WAYBEL_0:def 31; :: thesis: verum

end;

then A10: pk is directed-sups-preserving by WAYBEL_0:def 37;
subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;
then A11: subrelstr Lk is continuous LATTICE by A2, WAYBEL_5:28;
A12: the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def 15
.= rng pk by WAYBEL_1:44
.= the carrier of (subrelstr (rng pk)) by YELLOW_0:def 15 ;
subrelstr (rng pk) is full SubRelStr of L by Th1;
then A13: Image p = Image pk by A12, YELLOW_0:57;
subrelstr Lk is complete by A2, YELLOW_2:30;
hence Image p is continuous LATTICE by A11, A3, A13, A10, Th14; :: thesis: verum