let S, T be non empty Poset; :: thesis: for d being Function of T,S st T is complete & d is sups-preserving holds
ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
let d be Function of T,S; :: thesis: ( T is complete & d is sups-preserving implies ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
assume that
A1: T is complete and
A2: d is sups-preserving ; :: thesis: ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
defpred S₁[ set , set ] means ex s being Element of S st
( s = $1 & $2 = sup (d " (downarrow s)) );
A3: for e being set st e in the carrier of S holds
ex u being set st
( u in the carrier of T & S₁[e,u] )

proof

let e be set ; :: thesis: ( e in the carrier of S implies ex u being set st
( u in the carrier of T & S₁[e,u] ) )
assume e in the carrier of S ; :: thesis: ex u being set st
( u in the carrier of T & S₁[e,u] )
then reconsider s = e as Element of S ;
take sup (d " (downarrow s)) ; :: thesis: ( sup (d " (downarrow s)) in the carrier of T & S₁[e, sup (d " (downarrow s))] )
thus ( sup (d " (downarrow s)) in the carrier of T & S₁[e, sup (d " (downarrow s))] ) ; :: thesis: verum

end;

consider g being Function of the carrier of S,the carrier of T such that
A4: for e being set st e in the carrier of S holds
S₁[e,g . e] from FUNCT_2:sch 1(A3);
A5: for s being Element of S holds g . s = sup (d " (downarrow s))

proof

let s be Element of S; :: thesis: g . s = sup (d " (downarrow s))
ex s1 being Element of S st
( s1 = s & g . s = sup (d " (downarrow s1)) ) by A4;
hence g . s = sup (d " (downarrow s)) ; :: thesis: verum

end;

reconsider g = g as Function of S,T ;
take g ; :: thesis: ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
for X being Ideal of T holds d preserves_sup_of X by A2, WAYBEL_0:def 33;
then A6: d is monotone by WAYBEL_0:72;
A7: g is monotone

proof

let s1, s2 be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( s1 <= s2 implies g . s1 <= g . s2 )
A8: ex_sup_of d " (downarrow s1),T by A1, YELLOW_0:17;
A9: ex_sup_of d " (downarrow s2),T by A1, YELLOW_0:17;
assume s1 <= s2 ; :: thesis: g . s1 <= g . s2
then downarrow s1 c= downarrow s2 by WAYBEL_0:21;
then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A8, A9, RELAT_1:178, YELLOW_0:34;
then g . s1 <= sup (d " (downarrow s2)) by A5;
hence g . s1 <= g . s2 by A5; :: thesis: verum

end;

for t being Element of T
for s being Element of S holds
( s >= d . t iff g . s >= t )

proof

let t be Element of T; :: thesis: for s being Element of S holds
( s >= d . t iff g . s >= t )
let s be Element of S; :: thesis: ( s >= d . t iff g . s >= t )
A10: ex_sup_of d " (downarrow s),T by A1, YELLOW_0:17;
then sup (d " (downarrow s)) is_>=_than d " (downarrow s) by YELLOW_0:30;
then A11: g . s is_>=_than d " (downarrow s) by A5;

hereby :: thesis: ( g . s >= t implies s >= d . t )

assume s >= d . t ; :: thesis: g . s >= t
then d . t in downarrow s by WAYBEL_0:17;
then t in d " (downarrow s) by FUNCT_2:46;
hence g . s >= t by A11, LATTICE3:def 9; :: thesis: verum

end;

assume g . s >= t ; :: thesis: s >= d . t
then d . (g . s) >= d . t by A6, Def2;
then A12: d . (sup (d " (downarrow s))) >= d . t by A5;
d preserves_sup_of d " (downarrow s) by A2, WAYBEL_0:def 33;
then A13: ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A10, WAYBEL_0:def 31;
ex_sup_of downarrow s,S by WAYBEL_0:34;
then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A13, FUNCT_1:145, YELLOW_0:34;
then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:34;
hence s >= d . t by A12, ORDERS_2:26; :: thesis: verum

end;

hence [g,d] is Galois by A6, A7, Th9; :: thesis: for s being Element of S holds g . s is_maximum_of d " (downarrow s)
let s be Element of S; :: thesis: g . s is_maximum_of d " (downarrow s)
thus A14: ex_sup_of d " (downarrow s),T by A1, YELLOW_0:17; :: according to WAYBEL_1:def 7 :: thesis: ( g . s = "\/" (d " (downarrow s)),T & "\/" (d " (downarrow s)),T in d " (downarrow s) )
thus A15: g . s = sup (d " (downarrow s)) by A5; :: thesis: "\/" (d " (downarrow s)),T in d " (downarrow s)
d preserves_sup_of d " (downarrow s) by A2, WAYBEL_0:def 33;
then A16: ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A14, WAYBEL_0:def 31;
ex_sup_of downarrow s,S by WAYBEL_0:34;
then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A16, FUNCT_1:145, YELLOW_0:34;
then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:34;
then d . (g . s) <= s by A5;
then d . (g . s) in downarrow s by WAYBEL_0:17;
hence "\/" (d " (downarrow s)),T in d " (downarrow s) by A15, FUNCT_2:46; :: thesis: verum