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 : p . k <= k } as non empty Subset of by WAYBEL_1:46;
A2: subrelstr Lk is infs-inheriting by WAYBEL_1:53;
reconsider pk = p | Lk as Function of (subrelstr Lk),(subrelstr Lk) by WAYBEL_1:49;
A3: pk is kernel by WAYBEL_1:51;

now

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

now

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:162;
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)
A7: ex_sup_of X,L by YELLOW_0:17;
A8: subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:55;
then A9: ( dom pk = the carrier of (subrelstr Lk) & sup X' = sup X ) by A4, A7, FUNCT_2:def 1, WAYBEL_0:7;
( ex_sup_of p .: X,L & pk .: X is directed Subset of ) by A3, A4, YELLOW_0:17, YELLOW_2:17;
hence sup (pk .: X) = sup (p .: X) by A4, A8, A6, WAYBEL_0:7
.= p . (sup X') by A5, A7, WAYBEL_0:def 31
.= pk . (sup X) by A9, FUNCT_1:70 ;
:: 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:55;
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:47
.= 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:58;
subrelstr Lk is complete by A2, YELLOW_2:32;
hence Image p is continuous LATTICE by A11, A3, A13, A10, Th16; :: thesis: verum