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

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