let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
let g be Function of S,T; :: thesis: for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
let d be Function of T,S; :: thesis: ( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )

hereby :: thesis: ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) implies [g,d] is Galois )

assume A1: [g,d] is Galois ; :: thesis: ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
hence g is monotone by Th8; :: 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 d . t is_minimum_of g " (uparrow t) :: thesis: verum

proof

set X = g " (uparrow t);
t <= g . (d . t) by A1, Th8;
then g . (d . t) in uparrow t by WAYBEL_0:18;
then A2: d . t in g " (uparrow t) by FUNCT_2:38;
then A3: for s being Element of S st s is_<=_than g " (uparrow t) holds
d . t >= s ;
A4: d . t is_<=_than g " (uparrow t)

proof

let s be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not s in g " (uparrow t) or d . t <= s )
assume s in g " (uparrow t) ; :: thesis: d . t <= s
then g . s in uparrow t by FUNCT_1:def 7;
then t <= g . s by WAYBEL_0:18;
hence d . t <= s by A1, Th8; :: thesis: verum

end;

hence ( ex_inf_of g " (uparrow t),S & d . t = inf (g " (uparrow t)) ) by A3, YELLOW_0:31; :: according to WAYBEL_1:def 6 :: thesis: "/\" ((g " (uparrow t)),S) in g " (uparrow t)
thus "/\" ((g " (uparrow t)),S) in g " (uparrow t) by A4, A2, A3, YELLOW_0:31; :: thesis: verum

end;

end;

assume that
A5: g is monotone and
A6: for t being Element of T holds d . t is_minimum_of g " (uparrow t) ; :: thesis: [g,d] is Galois
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 )
set X = g " (uparrow t);

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 A8: s in g " (uparrow t) by FUNCT_2:38;
A9: d . t is_minimum_of g " (uparrow t) by A6;
then ex_inf_of g " (uparrow t),S ;
then g " (uparrow t) is_>=_than inf (g " (uparrow t)) by YELLOW_0:def 10;
then s >= inf (g " (uparrow t)) by A8;
hence d . t <= s by A9; :: thesis: verum

end;

A10: d . t is_minimum_of g " (uparrow t) by A6;
then inf (g " (uparrow t)) in g " (uparrow t) ;
then g . (inf (g " (uparrow t))) in uparrow t by FUNCT_1:def 7;
then g . (inf (g " (uparrow t))) >= t by WAYBEL_0:18;
then A11: g . (d . t) >= t by A10;
assume d . t <= s ; :: thesis: t <= g . s
then g . (d . t) <= g . s by A5;
hence t <= g . s by A11, ORDERS_2:3; :: thesis: verum

end;

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;
A13: d . t2 is_minimum_of g " (uparrow t2) by A6;
then A14: ex_inf_of g " (uparrow t2),S ;
A15: d . t1 is_minimum_of g " (uparrow t1) by A6;
then ex_inf_of g " (uparrow t1),S ;
then inf (g " (uparrow t1)) <= inf (g " (uparrow t2)) by A14, A12, RELAT_1:143, YELLOW_0:35;
then d . t1 <= inf (g " (uparrow t2)) by A15;
hence d . t1 <= d . t2 by A13; :: thesis: verum

end;

hence [g,d] is Galois by A5, A7; :: thesis: verum