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

proof

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

end;

g preserves_inf_of g " (uparrow t) by A2;
then ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A9;
then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A8, FUNCT_1:75, YELLOW_0:35;
then A11: g . (inf (g " (uparrow t))) >= t by WAYBEL_0:39;
assume d . t <= s ; :: thesis: t <= g . s
then g . (d . t) <= g . s by A6;
then g . (inf (g " (uparrow t))) <= g . s by A5;
hence t <= g . s by A11, ORDERS_2:3; :: thesis: verum

end;

take d ; :: thesis: ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
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 )
assume t1 <= t2 ; :: thesis: d . t1 <= d . t2
then A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22;
( ex_inf_of g " (uparrow t1),S & ex_inf_of g " (uparrow t2),S ) by A1, YELLOW_0:17;
then inf (g " (uparrow t1)) <= inf (g " (uparrow t2)) by A12, RELAT_1:143, YELLOW_0:35;
then d . t1 <= inf (g " (uparrow t2)) by A5;
hence d . t1 <= d . t2 by A5; :: thesis: verum

end;

hence [g,d] is Galois by A6, A7; :: 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 A13: 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 A14: d . t = inf (g " (uparrow t)) by A5; :: thesis: "/\" ((g " (uparrow t)),S) in g " (uparrow t)
A15: ex_inf_of uparrow t,T by WAYBEL_0:39;
g preserves_inf_of g " (uparrow t) by A2;
then ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A13;
then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A15, FUNCT_1:75, 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 A14, FUNCT_2:38; :: thesis: verum