let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}
let g be Function of S,T; :: thesis: for d being Function of T,S st [g,d] is Galois & d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}
let d be Function of T,S; :: thesis: ( [g,d] is Galois & d is onto implies for s being Element of S holds g . s is_maximum_of d " {s} )
assume that
A1: [g,d] is Galois and
A2: d is onto ; :: thesis: for s being Element of S holds g . s is_maximum_of d " {s}
let s be Element of S; :: thesis: g . s is_maximum_of d " {s}
A3: g . s is_maximum_of d " (downarrow s) by A1, Th12;
then A4: g . s = sup (d " (downarrow s)) by Def7;
A5: rng d = the carrier of S by A2, FUNCT_2:def 3;
then A6: d .: (d " (downarrow s)) = downarrow s by FUNCT_1:147;
consider t being set such that
A7: t in the carrier of T and
A8: d . t = s by A5, FUNCT_2:17;
reconsider t = t as Element of T by A7;
ex_sup_of d " (downarrow s),T by A3, Def7;
then A9: g . s is_>=_than d " (downarrow s) by A4, YELLOW_0:30;
A10: d is monotone by A1, Th9;
A11: {s} c= downarrow {s} by WAYBEL_0:16;
then A12: d " {s} c= d " (downarrow s) by RELAT_1:178;
A13: s in {s} by TARSKI:def 1;
then t in d " (downarrow s) by A8, A11, FUNCT_2:46;
then g . s >= t by A9, LATTICE3:def 9;
then A14: d . (g . s) >= s by A8, A10, Def2;
g . s in d " (downarrow s) by A3, A4, Def7;
then d . (g . s) in d .: (d " (downarrow s)) by FUNCT_2:43;
then s >= d . (g . s) by A6, WAYBEL_0:17;
then A15: d . (g . s) = s by A14, ORDERS_2:25;
A16: ex_sup_of d " (downarrow s),T by A3, Def7;
A17: g . s in d " {s} by A13, A15, FUNCT_2:46;
thus A18: ex_sup_of d " {s},T :: according to WAYBEL_1:def 7 :: thesis: ( g . s = "\/" (d " {s}),T & "\/" (d " {s}),T in d " {s} )

proof

take g . s ; :: according to YELLOW_0:def 7 :: thesis: ( d " {s} is_<=_than g . s & ( for b₁ being M2(the carrier of T) holds
( not d " {s} is_<=_than b₁ or g . s <= b₁ ) ) & ( for b₁ being M2(the carrier of T) holds
( not d " {s} is_<=_than b₁ or ex b₂ being M2(the carrier of T) st
( d " {s} is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = g . s ) ) )
thus A19: d " {s} is_<=_than g . s by A9, A12, YELLOW_0:9; :: thesis: ( ( for b₁ being M2(the carrier of T) holds
( not d " {s} is_<=_than b₁ or g . s <= b₁ ) ) & ( for b₁ being M2(the carrier of T) holds
( not d " {s} is_<=_than b₁ or ex b₂ being M2(the carrier of T) st
( d " {s} is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = g . s ) ) )
thus for b being Element of T st d " {s} is_<=_than b holds
b >= g . s by A17, LATTICE3:def 9; :: thesis: for b₁ being M2(the carrier of T) holds
( not d " {s} is_<=_than b₁ or ex b₂ being M2(the carrier of T) st
( d " {s} is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = g . s )
let c be Element of T; :: thesis: ( not d " {s} is_<=_than c or ex b₁ being M2(the carrier of T) st
( d " {s} is_<=_than b₁ & not c <= b₁ ) or c = g . s )
assume d " {s} is_<=_than c ; :: thesis: ( ex b₁ being M2(the carrier of T) st
( d " {s} is_<=_than b₁ & not c <= b₁ ) or c = g . s )
then A20: c >= g . s by A17, LATTICE3:def 9;
assume for b being Element of T st d " {s} is_<=_than b holds
b >= c ; :: thesis: c = g . s
then g . s >= c by A19;
hence c = g . s by A20, ORDERS_2:25; :: thesis: verum

end;

then A21: sup (d " {s}) <= g . s by A4, A11, A16, RELAT_1:178, YELLOW_0:34;
sup (d " {s}) is_>=_than d " {s} by A18, YELLOW_0:30;
then sup (d " {s}) >= g . s by A17, LATTICE3:def 9;
hence g . s = sup (d " {s}) by A21, ORDERS_2:25; :: thesis: "\/" (d " {s}),T in d " {s}
hence "\/" (d " {s}),T in d " {s} by A13, A15, FUNCT_2:46; :: thesis: verum