let R be complete Heyting LATTICE; :: thesis: for X being Subset of R
for y being Element of R holds ("\/" X,R) "/\" y = "\/" { (x "/\" y) where x is Element of R : x in X } ,R
let X be Subset of R; :: thesis: for y being Element of R holds ("\/" X,R) "/\" y = "\/" { (x "/\" y) where x is Element of R : x in X } ,R
let y be Element of R; :: thesis: ("\/" X,R) "/\" y = "\/" { (x "/\" y) where x is Element of R : x in X } ,R
set Z = { (y "/\" x) where x is Element of R : x in X } ;
set W = { (x "/\" y) where x is Element of R : x in X } ;
A1: { (x "/\" y) where x is Element of R : x in X } c= { (y "/\" x) where x is Element of R : x in X }

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in { (x "/\" y) where x is Element of R : x in X } or w in { (y "/\" x) where x is Element of R : x in X } )
assume w in { (x "/\" y) where x is Element of R : x in X } ; :: thesis: w in { (y "/\" x) where x is Element of R : x in X }
then ex x being Element of R st
( w = x "/\" y & x in X ) ;
hence w in { (y "/\" x) where x is Element of R : x in X } ; :: thesis: verum

end;

{ (y "/\" x) where x is Element of R : x in X } c= { (x "/\" y) where x is Element of R : x in X }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (y "/\" x) where x is Element of R : x in X } or z in { (x "/\" y) where x is Element of R : x in X } )
assume z in { (y "/\" x) where x is Element of R : x in X } ; :: thesis: z in { (x "/\" y) where x is Element of R : x in X }
then ex x being Element of R st
( z = y "/\" x & x in X ) ;
hence z in { (x "/\" y) where x is Element of R : x in X } ; :: thesis: verum

end;

then ( ( for z being Element of R holds
( z "/\" is lower_adjoint & ex_sup_of X,R ) ) & { (y "/\" x) where x is Element of R : x in X } = { (x "/\" y) where x is Element of R : x in X } ) by A1, WAYBEL_1:def 19, XBOOLE_0:def 10, YELLOW_0:17;
hence ("\/" X,R) "/\" y = "\/" { (x "/\" y) where x is Element of R : x in X } ,R by WAYBEL_1:66; :: thesis: verum