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₁[ object , object ] means ex s being Element of S st
( s = $1 & $2 = sup (d " (downarrow s)) );
A3: for e being object st e in the carrier of S holds
ex u being object st
( u in the carrier of T & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in the carrier of S implies ex u being object st
( u in the carrier of T & S₁[e,u] ) )
assume e in the carrier of S ; :: thesis: ex u being object 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 object 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 ;
for X being Ideal of T holds d preserves_sup_of X by A2;
then A6: d is monotone by WAYBEL_0:72;
A7: 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 )
A8: ex_sup_of downarrow s,S by WAYBEL_0:34;
A9: 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 A10: 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:38;
hence g . s >= t by A10; :: thesis: verum

end;

d preserves_sup_of d " (downarrow s) by A2;
then ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A9;
then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A8, FUNCT_1:75, YELLOW_0:34;
then A11: d . (sup (d " (downarrow s))) <= s by WAYBEL_0:34;
assume g . s >= t ; :: thesis: s >= d . t
then d . (g . s) >= d . t by A6;
then d . (sup (d " (downarrow s))) >= d . t by A5;
hence s >= d . t by A11, ORDERS_2:3; :: thesis: verum

end;

take g ; :: thesis: ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
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 )
assume s1 <= s2 ; :: thesis: g . s1 <= g . s2
then A12: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
( ex_sup_of d " (downarrow s1),T & ex_sup_of d " (downarrow s2),T ) by A1, YELLOW_0:17;
then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A12, RELAT_1:143, YELLOW_0:34;
then g . s1 <= sup (d " (downarrow s2)) by A5;
hence g . s1 <= g . s2 by A5; :: thesis: verum

end;

hence [g,d] is Galois by A6, A7; :: 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 A13: 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 A14: g . s = sup (d " (downarrow s)) by A5; :: thesis: "\/" ((d " (downarrow s)),T) in d " (downarrow s)
A15: ex_sup_of downarrow s,S by WAYBEL_0:34;
d preserves_sup_of d " (downarrow s) by A2;
then ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A13;
then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A15, FUNCT_1:75, 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 A14, FUNCT_2:38; :: thesis: verum