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:
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 (),() by WAYBEL_1:46;
A3: pk is kernel by WAYBEL_1:48;
now :: thesis: for X being Subset of () st not X is empty & X is directed holds
pk preserves_sup_of X
let X be Subset of (); :: 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:
then reconsider X9 = X9 as non empty directed Subset of L by YELLOW_2:7;
A5: p preserves_sup_of X9 by ;
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 () ;
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 ;
then A9: ( dom pk = the carrier of () & sup X9 = sup X ) by ;
( ex_sup_of p .: X,L & pk .: X is directed Subset of () ) by ;
hence sup (pk .: X) = sup (p .: X) by
.= p . (sup X9) by
.= pk . (sup X) by ;
:: 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 ;
then A11: subrelstr Lk is continuous LATTICE by ;
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 ;
subrelstr Lk is complete by ;
hence Image p is continuous LATTICE by A11, A3, A13, A10, Th14; :: thesis: verum