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 Th63, 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 Th61 ; :: thesis: verum

end;

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