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