let L be complete Boolean LATTICE; :: thesis: for X being Subset of
for x being Element of holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of : y in X } ,L
let X be Subset of ; :: thesis: for x being Element of holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of : y in X } ,L
let x be Element of ; :: thesis: x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of : y in X } ,L
for y being Element of holds y "/\" is lower_adjoint by WAYBEL_1:def 19;
hence x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of : y in X } ,L by WAYBEL_1:67; :: thesis: verum