let L be lower-bounded continuous sup-Semilattice; :: thesis: SupMap L is upper_adjoint
set P = InclPoset (Ids L);
set r = SupMap L;
deffunc H₁( Element of ) -> Element of the carrier of (InclPoset (Ids L)) = inf ((SupMap L) " (uparrow {$1}));
ex d being Function of L,(InclPoset (Ids L)) st
for t being Element of holds d . t = H₁(t) from FUNCT_2:sch 4();
then consider d being Function of L,(InclPoset (Ids L)) such that
A1: for t being Element of holds d . t = inf ((SupMap L) " (uparrow {t})) ;
for t being Element of holds d . t is_minimum_of (SupMap L) " (uparrow t)

proof

let t be Element of ; :: thesis: d . t is_minimum_of (SupMap L) " (uparrow t)
set I = inf ((SupMap L) " (uparrow t));
reconsider I' = inf ((SupMap L) " (uparrow t)) as Ideal of L by YELLOW_2:43;
A2: d . t = inf ((SupMap L) " (uparrow {t})) by A1
.= inf ((SupMap L) " (uparrow t)) by WAYBEL_0:def 18 ;
inf ((SupMap L) " (uparrow t)) in the carrier of (InclPoset (Ids L)) ;
then inf ((SupMap L) " (uparrow t)) in Ids L by YELLOW_1:1;
then A3: inf ((SupMap L) " (uparrow t)) in dom (SupMap L) by YELLOW_2:51;
consider J being Ideal of L such that
A4: t <= sup J and
A5: for K being Ideal of L st t <= sup K holds
J c= K by Lm3;
reconsider J' = J as Element of by YELLOW_2:43;
A6: for K being Element of st (SupMap L) " (uparrow t) is_>=_than K holds
K <= J'

proof

J' in the carrier of (InclPoset (Ids L)) ;
then J' in Ids L by YELLOW_1:1;
then A7: J in dom (SupMap L) by YELLOW_2:51;
let K be Element of ; :: thesis: ( (SupMap L) " (uparrow t) is_>=_than K implies K <= J' )
assume A8: (SupMap L) " (uparrow t) is_>=_than K ; :: thesis: K <= J'
t <= (SupMap L) . J' by A4, YELLOW_2:def 3;
then (SupMap L) . J in uparrow t by WAYBEL_0:18;
then J in (SupMap L) " (uparrow t) by A7, FUNCT_1:def 13;
hence K <= J' by A8, LATTICE3:def 8; :: thesis: verum

end;

(SupMap L) " (uparrow t) is_>=_than J'

proof

let K be Element of ; :: according to LATTICE3:def 8 :: thesis: ( not K in (SupMap L) " (uparrow t) or J' <= K )
reconsider K' = K as Ideal of L by YELLOW_2:43;
assume K in (SupMap L) " (uparrow t) ; :: thesis: J' <= K
then (SupMap L) . K in uparrow t by FUNCT_1:def 13;
then t <= (SupMap L) . K by WAYBEL_0:18;
then t <= sup K' by YELLOW_2:def 3;
then J' c= K' by A5;
hence J' <= K by YELLOW_1:3; :: thesis: verum

end;

then t <= sup I' by A4, A6, YELLOW_0:31;
then t <= (SupMap L) . (inf ((SupMap L) " (uparrow t))) by YELLOW_2:def 3;
then (SupMap L) . (inf ((SupMap L) " (uparrow t))) in uparrow t by WAYBEL_0:18;
then ( ex_inf_of (SupMap L) " (uparrow t), InclPoset (Ids L) & inf ((SupMap L) " (uparrow t)) in (SupMap L) " (uparrow t) ) by A3, FUNCT_1:def 13, YELLOW_0:17;
hence d . t is_minimum_of (SupMap L) " (uparrow t) by A2, WAYBEL_1:def 6; :: thesis: verum

end;

then [(SupMap L),d] is Galois by WAYBEL_1:11;
hence SupMap L is upper_adjoint by WAYBEL_1:def 11; :: thesis: verum