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:46;
A2: subrelstr Lk is infs-inheriting by WAYBEL_1:53;
subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:55;
then A3: subrelstr Lk is continuous LATTICE by A2, WAYBEL_5:28;
A4: subrelstr Lk is complete by A2, YELLOW_2:32;
reconsider pk = p | Lk as Function of (subrelstr Lk),(subrelstr Lk) by WAYBEL_1:49;
A5: pk is kernel by WAYBEL_1:51;
A6: subrelstr (rng pk) is full SubRelStr of L by Th1;
the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def 15
.= rng pk by WAYBEL_1:47
.= the carrier of (subrelstr (rng pk)) by YELLOW_0:def 15 ;
then A7: Image p = Image pk by A6, YELLOW_0:58;

now

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

now

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:53;
then subrelstr Lk is complete LATTICE by YELLOW_2:32;
hence ex_sup_of pk .: X, subrelstr Lk by YELLOW_0:17; :: thesis: sup (pk .: X) = pk . (sup X)
A10: dom pk = the carrier of (subrelstr Lk) by FUNCT_2:def 1;
A11: ex_sup_of X,L by YELLOW_0:17;
A12: ex_sup_of p .: X,L by YELLOW_0:17;
A13: pk .: X is directed Subset of (subrelstr Lk) by A8, A5, YELLOW_2:17;
A15: subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:55;
then A16: sup X' = sup X by A8, A11, WAYBEL_0:7;
X c= the carrier of (subrelstr Lk) ;
then X c= Lk by YELLOW_0:def 15;
then pk .: X = p .: X by RELAT_1:162;
hence sup (pk .: X) = sup (p .: X) by A12, A13, A8, A15, WAYBEL_0:7
.= p . (sup X') by A9, A11, WAYBEL_0:def 31
.= pk . (sup X) by A10, A16, FUNCT_1:70 ;
:: thesis: verum

end;

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

end;

then pk is directed-sups-preserving by WAYBEL_0:def 37;
hence Image p is continuous LATTICE by A3, A4, A5, A7, Th16; :: thesis: verum