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 L) -> 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 L 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 L holds d . t = inf ((SupMap L) " (uparrow {t})) ;
for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t)

proof

let t be Element of L; :: thesis: d . t is_minimum_of (SupMap L) " (uparrow t)
set I = inf ((SupMap L) " (uparrow t));
reconsider I9 = inf ((SupMap L) " (uparrow t)) as Ideal of L by YELLOW_2:41;
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:49;
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 J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41;
A6: for K being Element of (InclPoset (Ids L)) st (SupMap L) " (uparrow t) is_>=_than K holds
K <= J9

proof

J9 in the carrier of (InclPoset (Ids L)) ;
then J9 in Ids L by YELLOW_1:1;
then A7: J in dom (SupMap L) by YELLOW_2:49;
let K be Element of (InclPoset (Ids L)); :: thesis: ( (SupMap L) " (uparrow t) is_>=_than K implies K <= J9 )
assume A8: (SupMap L) " (uparrow t) is_>=_than K ; :: thesis: K <= J9
t <= (SupMap L) . J9 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 7;
hence K <= J9 by A8; :: thesis: verum

end;

(SupMap L) " (uparrow t) is_>=_than J9

proof

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

end;

then t <= sup I9 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 7, 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:10;
hence SupMap L is upper_adjoint by WAYBEL_1:def 11; :: thesis: verum