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 :: thesis: for X being Subset of L st not X is empty & X is directed holds
corestr p preserves_sup_of X

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 A2: p preserves_sup_of X by A1, WAYBEL_0:def 37;
A3: Image p is sups-inheriting by WAYBEL_1:53;

now :: thesis: ( ex_sup_of X,L implies ( ex_sup_of (corestr p) .: X, Image p & sup ((corestr p) .: X) = (corestr p) . (sup X) ) )

assume A4: 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:54;
hence ex_sup_of (corestr p) .: X, Image p by YELLOW_0:17; :: thesis: sup ((corestr p) .: X) = (corestr p) . (sup X)
A5: (corestr p) .: X = p .: X by WAYBEL_1:30;
ex_sup_of p .: X,L by YELLOW_0:17;
then "\/" (((corestr p) .: X),L) in the carrier of (Image p) by A3, A5, YELLOW_0:def 19;
hence sup ((corestr p) .: X) = sup (p .: X) by A5, YELLOW_0:68
.= p . (sup X) by A2, A4, WAYBEL_0:def 31
.= (corestr p) . (sup X) by WAYBEL_1:30 ;
:: 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:56, WAYBEL_5:33; :: thesis: verum