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 Th9; :: 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);
A2: 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 13;
then s >= d . t by WAYBEL_0:17;
hence t <= g . s by A1, Th9; :: thesis: verum

end;

s >= d . (g . s) by A1, Th9;
then d . (g . s) in downarrow s by WAYBEL_0:17;
then A3: g . s in d " (downarrow s) by FUNCT_2:46;
then A4: for t being Element of T st t is_>=_than d " (downarrow s) holds
g . s <= t by LATTICE3:def 9;
hence ( ex_sup_of d " (downarrow s),T & g . s = sup (d " (downarrow s)) ) by A2, 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 A2, A3, A4, 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: 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 A8: s1 <= s2 ; :: thesis: g . s1 <= g . s2
A9: g . s1 is_maximum_of d " (downarrow s1) by A6;
then A10: ex_sup_of d " (downarrow s1),T by Def7;
A11: g . s2 is_maximum_of d " (downarrow s2) by A6;
then A12: ex_sup_of d " (downarrow s2),T by Def7;
downarrow s1 c= downarrow s2 by A8, WAYBEL_0:21;
then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A10, A12, RELAT_1:178, YELLOW_0:34;
then g . s1 <= sup (d " (downarrow s2)) by A9, Def7;
hence g . s1 <= g . s2 by A11, Def7; :: thesis: verum

end;

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);
A13: g . s is_maximum_of d " (downarrow s) by A6;

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

end;

assume g . s >= t ; :: thesis: s >= d . t
then A15: d . (g . s) >= d . t by A5, Def2;
sup (d " (downarrow s)) in d " (downarrow s) by A13, Def7;
then d . (sup (d " (downarrow s))) in downarrow s by FUNCT_1:def 13;
then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:17;
then d . (g . s) <= s by A13, Def7;
hence s >= d . t by A15, ORDERS_2:26; :: thesis: verum

end;

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