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}
A3: d is monotone by A1, Th9;
let s be Element of S; :: thesis: g . s is_maximum_of d " {s}
A4: rng d = the carrier of S by A2, FUNCT_2:def 3;
then A5: d .: (d " (downarrow s)) = downarrow s by FUNCT_1:147;
A6: g . s is_maximum_of d " (downarrow s) by A1, Th12;
then A7: g . s = sup (d " (downarrow s)) by Def7;
then g . s in d " (downarrow s) by A6, Def7;
then d . (g . s) in d .: (d " (downarrow s)) by FUNCT_2:43;
then A8: s >= d . (g . s) by A5, WAYBEL_0:17;
ex_sup_of d " (downarrow s),T by A6, Def7;
then A9: g . s is_>=_than d " (downarrow s) by A7, YELLOW_0:30;
consider t being set such that
A10: t in the carrier of T and
A11: d . t = s by A4, FUNCT_2:17;
reconsider t = t as Element of T by A10;
A12: s in {s} by TARSKI:def 1;
A13: {s} c= downarrow {s} by WAYBEL_0:16;
then t in d " (downarrow s) by A11, A12, FUNCT_2:46;
then g . s >= t by A9, LATTICE3:def 9;
then d . (g . s) >= s by A11, A3, Def2;
then A14: d . (g . s) = s by A8, ORDERS_2:25;
then A15: g . s in d " {s} by A12, FUNCT_2:46;
A16: d " {s} c= d " (downarrow s) by RELAT_1:178, WAYBEL_0:16;
thus A17: 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 d " {s} is_<=_than g . s by A9, A16, 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 A15, 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 A18: c >= g . s by A15, 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 A9, A16, YELLOW_0:9;
hence c = g . s by A18, ORDERS_2:25; :: thesis: verum

end;

then sup (d " {s}) is_>=_than d " {s} by YELLOW_0:30;
then A19: sup (d " {s}) >= g . s by A15, LATTICE3:def 9;
ex_sup_of d " (downarrow s),T by A6, Def7;
then sup (d " {s}) <= g . s by A7, A13, A17, RELAT_1:178, YELLOW_0:34;
hence g . s = sup (d " {s}) by A19, ORDERS_2:25; :: thesis: "\/" ((d " {s}),T) in d " {s}
hence "\/" ((d " {s}),T) in d " {s} by A12, A14, FUNCT_2:46; :: thesis: verum