let S be Semilattice; :: thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) implies for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )
assume A1: for x being Element of S holds x "/\" is lower_adjoint ; :: thesis: for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)
let X be Subset of S; :: thesis: ( ex_sup_of X,S implies for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )
assume A2: ex_sup_of X,S ; :: thesis: for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)
let x be Element of S; :: thesis: x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)
x "/\" is sups-preserving by A1, Th13;
then x "/\" preserves_sup_of X ;
then sup ((x "/\") .: X) = (x "/\") . (sup X) by A2;
hence x "/\" ("\/" (X,S)) = sup ((x "/\") .: X) by Def18
.= "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) by Th61 ;
:: thesis: verum