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