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

proof

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

end;

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

proof

let t be Element of T; :: thesis: d . t = inf (g " (uparrow t))
ex t1 being Element of T st
( t1 = t & d . t = inf (g " (uparrow t1)) ) by A4;
hence d . t = inf (g " (uparrow t)) ; :: thesis: verum

end;

reconsider d = d as Function of T,S ;
take d ; :: thesis: ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
for X being Filter of S holds g preserves_inf_of X by A2, WAYBEL_0:def 32;
then A6: g is monotone by WAYBEL_0:69;
A7: d is monotone

proof

let t1, t2 be Element of T; :: according to WAYBEL_1:def 2 :: thesis: ( t1 <= t2 implies d . t1 <= d . t2 )
A8: ex_inf_of g " (uparrow t1),S by A1, YELLOW_0:17;
A9: ex_inf_of g " (uparrow t2),S by A1, YELLOW_0:17;
assume t1 <= t2 ; :: thesis: d . t1 <= d . t2
then uparrow t2 c= uparrow t1 by WAYBEL_0:22;
then inf (g " (uparrow t1)) <= inf (g " (uparrow t2)) by A8, A9, RELAT_1:178, YELLOW_0:35;
then d . t1 <= inf (g " (uparrow t2)) by A5;
hence d . t1 <= d . t2 by A5; :: thesis: verum

end;

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

proof

let t be Element of T; :: thesis: for s being Element of S holds
( t <= g . s iff d . t <= s )
let s be Element of S; :: thesis: ( t <= g . s iff d . t <= s )
A10: ex_inf_of g " (uparrow t),S by A1, YELLOW_0:17;
then inf (g " (uparrow t)) is_<=_than g " (uparrow t) by YELLOW_0:31;
then A11: d . t is_<=_than g " (uparrow t) by A5;

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

assume t <= g . s ; :: thesis: d . t <= s
then g . s in uparrow t by WAYBEL_0:18;
then s in g " (uparrow t) by FUNCT_2:46;
hence d . t <= s by A11, LATTICE3:def 8; :: thesis: verum

end;

assume d . t <= s ; :: thesis: t <= g . s
then g . (d . t) <= g . s by A6, Def2;
then A12: g . (inf (g " (uparrow t))) <= g . s by A5;
g preserves_inf_of g " (uparrow t) by A2, WAYBEL_0:def 32;
then A13: ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A10, WAYBEL_0:def 30;
ex_inf_of uparrow t,T by WAYBEL_0:39;
then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A13, FUNCT_1:145, YELLOW_0:35;
then g . (inf (g " (uparrow t))) >= t by WAYBEL_0:39;
hence t <= g . s by A12, ORDERS_2:26; :: thesis: verum

end;

hence [g,d] is Galois by A6, A7, Th9; :: thesis: for t being Element of T holds d . t is_minimum_of g " (uparrow t)
let t be Element of T; :: thesis: d . t is_minimum_of g " (uparrow t)
thus A14: ex_inf_of g " (uparrow t),S by A1, YELLOW_0:17; :: according to WAYBEL_1:def 6 :: thesis: ( d . t = "/\" (g " (uparrow t)),S & "/\" (g " (uparrow t)),S in g " (uparrow t) )
thus A15: d . t = inf (g " (uparrow t)) by A5; :: thesis: "/\" (g " (uparrow t)),S in g " (uparrow t)
g preserves_inf_of g " (uparrow t) by A2, WAYBEL_0:def 32;
then A16: ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A14, WAYBEL_0:def 30;
ex_inf_of uparrow t,T by WAYBEL_0:39;
then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A16, FUNCT_1:145, YELLOW_0:35;
then g . (inf (g " (uparrow t))) >= t by WAYBEL_0:39;
then g . (d . t) >= t by A5;
then g . (d . t) in uparrow t by WAYBEL_0:18;
hence "/\" (g " (uparrow t)),S in g " (uparrow t) by A15, FUNCT_2:46; :: thesis: verum