let S be non empty complete Poset; :: thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for X being Subset of S
for x being Element of S holds x "/\" ("\/" X,S) = "\/" { (x "/\" y) where y is Element of S : y in X } ,S )
thus ( ( for x being Element of S holds x "/\" is lower_adjoint ) implies for X being Subset of S
for x being Element of S holds x "/\" ("\/" X,S) = "\/" { (x "/\" y) where y is Element of S : y in X } ,S ) by Th66, YELLOW_0:17; :: thesis: ( ( for X being Subset of S
for x being Element of S holds x "/\" ("\/" X,S) = "\/" { (x "/\" y) where y is Element of S : y in X } ,S ) implies for x being Element of S holds x "/\" is lower_adjoint )
assume A1: for X being Subset of S
for x being Element of S holds x "/\" ("\/" X,S) = "\/" { (x "/\" y) where y is Element of S : y in X } ,S ; :: thesis: for x being Element of S holds x "/\" is lower_adjoint
let x be Element of S; :: thesis: x "/\" is lower_adjoint
x "/\" is sups-preserving

proof

let X be Subset of S; :: according to WAYBEL_0:def 33 :: thesis: x "/\" preserves_sup_of X
assume ex_sup_of X,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (x "/\" ) .: X,S & "\/" ((x "/\" ) .: X),S = (x "/\" ) . ("\/" X,S) )
thus ex_sup_of (x "/\" ) .: X,S by YELLOW_0:17; :: thesis: "\/" ((x "/\" ) .: X),S = (x "/\" ) . ("\/" X,S)
thus (x "/\" ) . (sup X) = x "/\" ("\/" X,S) by Def18
.= "\/" { (x "/\" y) where y is Element of S : y in X } ,S by A1
.= sup ((x "/\" ) .: X) by Th64 ; :: thesis: verum

end;

hence x "/\" is lower_adjoint by Th18; :: thesis: verum