let S be Semilattice; :: thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S )

hereby :: thesis: ( ( for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ) implies for x being Element of S holds x "/\" is lower_adjoint )

assume A1: for x being Element of S holds x "/\" is lower_adjoint ; :: thesis: for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S
let x, t be Element of S; :: thesis: ex_max_of { s where s is Element of S : x "/\" s <= t } ,S
set X = { s where s is Element of S : x "/\" s <= t } ;
x "/\" is lower_adjoint by A1;
then consider g being Function of S,S such that
A2: [g,(x "/\" )] is Galois by Def12;
A3: { s where s is Element of S : x "/\" s <= t } = (x "/\" ) " (downarrow t) by Th62;
g . t is_maximum_of (x "/\" ) " (downarrow t) by A2, Th12;
then ( ex_sup_of { s where s is Element of S : x "/\" s <= t } ,S & "\/" { s where s is Element of S : x "/\" s <= t } ,S in { s where s is Element of S : x "/\" s <= t } ) by A3, Def7;
hence ex_max_of { s where s is Element of S : x "/\" s <= t } ,S by Def5; :: thesis: verum

end;

assume A4: for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ; :: thesis: for x being Element of S holds x "/\" is lower_adjoint
let x be Element of S; :: thesis: x "/\" is lower_adjoint
deffunc H₁( Element of S) -> M2(the carrier of S) = "\/" ((x "/\" ) " (downarrow $1)),S;
consider g being Function of S,S such that
A5: for s being Element of S holds g . s = H₁(s) from FUNCT_2:sch 4();

now

let t be Element of S; :: thesis: g . t is_maximum_of (x "/\" ) " (downarrow t)
set X = { s where s is Element of S : x "/\" s <= t } ;
ex_max_of { s where s is Element of S : x "/\" s <= t } ,S by A4;
then A6: ( ex_sup_of { s where s is Element of S : x "/\" s <= t } ,S & "\/" { s where s is Element of S : x "/\" s <= t } ,S in { s where s is Element of S : x "/\" s <= t } ) by Def5;
A7: { s where s is Element of S : x "/\" s <= t } = (x "/\" ) " (downarrow t) by Th62;
g . t = "\/" ((x "/\" ) " (downarrow t)),S by A5;
hence g . t is_maximum_of (x "/\" ) " (downarrow t) by A6, A7, Def7; :: thesis: verum

end;

then [g,(x "/\" )] is Galois by Th12;
hence x "/\" is lower_adjoint by Def12; :: thesis: verum