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 & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
let g be Function of S,T; :: thesis: for d being Function of T,S st [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
let d be Function of T,S; :: thesis: ( [g,d] is Galois & g is onto implies for t being Element of T holds d . t is_minimum_of g " {t} )
assume that
A1: [g,d] is Galois and
A2: g is onto ; :: thesis: for t being Element of T holds d . t is_minimum_of g " {t}
let t be Element of T; :: thesis: d . t is_minimum_of g " {t}
A3: d . t is_minimum_of g " (uparrow t) by A1, Th11;
then A4: d . t = inf (g " (uparrow t)) by Def6;
A5: rng g = the carrier of T by A2, FUNCT_2:def 3;
then A6: g .: (g " (uparrow t)) = uparrow t by FUNCT_1:147;
consider s being set such that
A7: s in the carrier of S and
A8: g . s = t by A5, FUNCT_2:17;
reconsider s = s as Element of S by A7;
ex_inf_of g " (uparrow t),S by A3, Def6;
then A9: d . t is_<=_than g " (uparrow t) by A4, YELLOW_0:31;
A10: g is monotone by A1, Th9;
A11: {t} c= uparrow {t} by WAYBEL_0:16;
then A12: g " {t} c= g " (uparrow t) by RELAT_1:178;
A13: t in {t} by TARSKI:def 1;
then s in g " (uparrow t) by A8, A11, FUNCT_2:46;
then d . t <= s by A9, LATTICE3:def 8;
then A14: g . (d . t) <= t by A8, A10, Def2;
d . t in g " (uparrow t) by A3, A4, Def6;
then g . (d . t) in g .: (g " (uparrow t)) by FUNCT_2:43;
then t <= g . (d . t) by A6, WAYBEL_0:18;
then A15: g . (d . t) = t by A14, ORDERS_2:25;
A16: ex_inf_of g " (uparrow t),S by A3, Def6;
A17: d . t in g " {t} by A13, A15, FUNCT_2:46;
thus A18: ex_inf_of g " {t},S :: according to WAYBEL_1:def 6 :: thesis: ( d . t = "/\" (g " {t}),S & "/\" (g " {t}),S in g " {t} )

proof

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

end;

then A21: inf (g " {t}) >= d . t by A4, A11, A16, RELAT_1:178, YELLOW_0:35;
inf (g " {t}) is_<=_than g " {t} by A18, YELLOW_0:31;
then inf (g " {t}) <= d . t by A17, LATTICE3:def 8;
hence d . t = inf (g " {t}) by A21, ORDERS_2:25; :: thesis: "/\" (g " {t}),S in g " {t}
hence "/\" (g " {t}),S in g " {t} by A13, A15, FUNCT_2:46; :: thesis: verum