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, Th14;
then x "/\" preserves_sup_of X by WAYBEL_0:def 33;
then sup ((x "/\" ) .: X) = (x "/\" ) . (sup X) by A2, WAYBEL_0:def 31;
hence x "/\" ("\/" X,S) = sup ((x "/\" ) .: X) by Def18
.= "\/" { (x "/\" y) where y is Element of S : y in X } ,S by Th64 ;
:: thesis: verum