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