let L be lower-bounded continuous sup-Semilattice; :: thesis:
set P = InclPoset (Ids L);
set r = SupMap L;
deffunc H1( Element of L) -> Element of the carrier of (InclPoset (Ids L)) = inf (() " ());
ex d being Function of L,(InclPoset (Ids L)) st
for t being Element of L holds d . t = H1(t) from then consider d being Function of L,(InclPoset (Ids L)) such that
A1: for t being Element of L holds d . t = inf (() " ()) ;
for t being Element of L holds d . t is_minimum_of () " ()
proof
let t be Element of L; :: thesis: d . t is_minimum_of () " ()
set I = inf (() " ());
reconsider I9 = inf (() " ()) as Ideal of L by YELLOW_2:41;
A2: d . t = inf (() " ()) by A1
.= inf (() " ()) by WAYBEL_0:def 18 ;
inf (() " ()) in the carrier of (InclPoset (Ids L)) ;
then inf (() " ()) in Ids L by YELLOW_1:1;
then A3: inf (() " ()) in dom () 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 () " () 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 () by YELLOW_2:49;
let K be Element of (InclPoset (Ids L)); :: thesis: ( () " () is_>=_than K implies K <= J9 )
assume A8: (SupMap L) " () is_>=_than K ; :: thesis: K <= J9
t <= () . J9 by ;
then (SupMap L) . J in uparrow t by WAYBEL_0:18;
then J in () " () by ;
hence K <= J9 by A8; :: thesis: verum
end;
(SupMap L) " () is_>=_than J9
proof
let K be Element of (InclPoset (Ids L)); :: according to LATTICE3:def 8 :: thesis: ( not K in () " () or J9 <= K )
reconsider K9 = K as Ideal of L by YELLOW_2:41;
assume K in () " () ; :: thesis: J9 <= K
then (SupMap L) . K in uparrow t by FUNCT_1:def 7;
then t <= () . 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 ;
then t <= () . (inf (() " ())) by YELLOW_2:def 3;
then (SupMap L) . (inf (() " ())) in uparrow t by WAYBEL_0:18;
then ( ex_inf_of () " (), InclPoset (Ids L) & inf (() " ()) in () " () ) by ;
hence d . t is_minimum_of () " () by ; :: thesis: verum
end;
then [(),d] is Galois by WAYBEL_1:10;
hence SupMap L is upper_adjoint by WAYBEL_1:def 11; :: thesis: verum