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

hence Image p is continuous LATTICE by WAYBEL_1:56, WAYBEL_5:33; :: thesis: verum

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

then
corestr p is directed-sups-preserving
by WAYBEL_0:def 37;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;

end;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) ) )

hence
corestr p preserves_sup_of X
by WAYBEL_0:def 31; :: thesis: verumassume 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;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

hence Image p is continuous LATTICE by WAYBEL_1:56, WAYBEL_5:33; :: thesis: verum