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));
A2: ex_inf_of (SupMap L) " (uparrow t), InclPoset (Ids L) by YELLOW_0:17;
A3: 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 A4: inf ((SupMap L) " (uparrow t)) in dom (SupMap L) by YELLOW_2:51;
reconsider I' = inf ((SupMap L) " (uparrow t)) as Ideal of L by YELLOW_2:43;
consider J being Ideal of L such that
A5: t <= sup J and
A6: for K being Ideal of L st t <= sup K holds
J c= K by Lm3;
reconsider J' = J as Element of (InclPoset (Ids L)) by YELLOW_2:43;
A7: (SupMap L) " (uparrow t) is_>=_than J'

proof

let K be Element of (InclPoset (Ids L)); :: 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 ( K in dom (SupMap L) & (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 A6;
hence J' <= K by YELLOW_1:3; :: thesis: verum

end;

for K being Element of (InclPoset (Ids L)) st (SupMap L) " (uparrow t) is_>=_than K holds
K <= J'

proof

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

end;

then t <= sup I' by A5, A7, 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 inf ((SupMap L) " (uparrow t)) in (SupMap L) " (uparrow t) by A4, FUNCT_1:def 13;
hence d . t is_minimum_of (SupMap L) " (uparrow t) by A2, A3, 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