let L be complete continuous LATTICE; :: thesis: for p being kernel Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
let p be kernel 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

now

let X be Subset of L; :: thesis: ( not X is empty & X is directed implies corestr p preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: corestr p preserves_sup_of X
then A3: p preserves_sup_of X by A1, WAYBEL_0:def 37;
A4: Image p is sups-inheriting by WAYBEL_1:56;

now

assume A5: ex_sup_of X,L ; :: thesis: ( ex_sup_of (corestr p) .: X, Image p & sup ((corestr p) .: X) = (corestr p) . (sup X) )
Image p is complete by WAYBEL_1:57;
hence ex_sup_of (corestr p) .: X, Image p by YELLOW_0:17; :: thesis: sup ((corestr p) .: X) = (corestr p) . (sup X)
A6: (corestr p) .: X = p .: X by WAYBEL_1:32;
ex_sup_of p .: X,L by YELLOW_0:17;
then "\/" ((corestr p) .: X),L in the carrier of (Image p) by A4, A6, YELLOW_0:def 19;
hence sup ((corestr p) .: X) = sup (p .: X) by A6, YELLOW_0:69
.= p . (sup X) by A3, A5, WAYBEL_0:def 31
.= (corestr p) . (sup X) by WAYBEL_1:32 ;
:: thesis: verum

end;

hence corestr p preserves_sup_of X by WAYBEL_0:def 31; :: thesis: verum

end;

then corestr p is directed-sups-preserving by WAYBEL_0:def 37;
hence Image p is continuous LATTICE by WAYBEL_1:59, WAYBEL_5:33; :: thesis: verum