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:64; :: thesis: verum