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
x "/\" is lower_adjoint by A1;
then consider g being Function of S,S such that
A2: [g,(x "/\")] is Galois ;
set X = { s where s is Element of S : x "/\" s <= t } ;
A3: { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) by Th59;
g . t is_maximum_of (x "/\") " (downarrow t) by A2, Th11;
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;
hence ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ; :: 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) -> M3( 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 :: thesis: for t being Element of S holds g . t is_maximum_of (x "/\") " (downarrow t)

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 } ) ;
( { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) & g . t = "\/" (((x "/\") " (downarrow t)),S) ) by A5, Th59;
hence g . t is_maximum_of (x "/\") " (downarrow t) by A6; :: thesis: verum

end;

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