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

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