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