let L be complete Semilattice; :: thesis: ( SupMap L is infs-preserving & SupMap L is sups-preserving implies SupMap L is upper_adjoint )
set r = SupMap L;
assume ( SupMap L is infs-preserving & SupMap L is sups-preserving ) ; :: thesis: SupMap L is upper_adjoint
then ex d being Function of L,(InclPoset (Ids L)) st
( [(SupMap L),d] is Galois & ( for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t) ) ) by WAYBEL_1:14;
hence SupMap L is upper_adjoint by WAYBEL_1:def 11; :: thesis: verum