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 ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
let g be Function of S,T; :: thesis: for d being Function of T,S holds
( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
let d be Function of T,S; :: thesis: ( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )

hereby :: thesis: ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) implies [g,d] is Galois )

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

proof

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

proof

let t be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not t in d " (downarrow s) or t <= g . s )
assume t in d " (downarrow s) ; :: thesis: t <= g . s
then d . t in downarrow s by FUNCT_1:def 7;
then s >= d . t by WAYBEL_0:17;
hence t <= g . s by A1, Th8; :: thesis: verum

end;

hence ( ex_sup_of d " (downarrow s),T & g . s = sup (d " (downarrow s)) ) by A3, YELLOW_0:30; :: according to WAYBEL_1:def 7 :: thesis: "\/" ((d " (downarrow s)),T) in d " (downarrow s)
thus "\/" ((d " (downarrow s)),T) in d " (downarrow s) by A4, A2, A3, YELLOW_0:30; :: thesis: verum

end;

end;

assume that
A5: d is monotone and
A6: for s being Element of S holds g . s is_maximum_of d " (downarrow s) ; :: thesis: [g,d] is Galois
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 )
set X = d " (downarrow s);
A8: g . s is_maximum_of d " (downarrow s) by A6;
then sup (d " (downarrow s)) in d " (downarrow s) ;
then d . (sup (d " (downarrow s))) in downarrow s by FUNCT_1:def 7;
then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:17;
then A9: d . (g . s) <= s by A8;

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 A10: t in d " (downarrow s) by FUNCT_2:38;
ex_sup_of d " (downarrow s),T by A8;
then d " (downarrow s) is_<=_than sup (d " (downarrow s)) by YELLOW_0:def 9;
then t <= sup (d " (downarrow s)) by A10;
hence g . s >= t by A8; :: thesis: verum

end;

assume g . s >= t ; :: thesis: s >= d . t
then d . (g . s) >= d . t by A5;
hence s >= d . t by A9, ORDERS_2:3; :: thesis: verum

end;

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 A11: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
A12: g . s2 is_maximum_of d " (downarrow s2) by A6;
then A13: ex_sup_of d " (downarrow s2),T ;
A14: g . s1 is_maximum_of d " (downarrow s1) by A6;
then ex_sup_of d " (downarrow s1),T ;
then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A13, A11, RELAT_1:143, YELLOW_0:34;
then g . s1 <= sup (d " (downarrow s2)) by A14;
hence g . s1 <= g . s2 by A12; :: thesis: verum

end;

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