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
A1: for z being Element of R holds
( z "/\" is lower_adjoint & ex_sup_of X,R ) by WAYBEL_1:def 19, YELLOW_0:17;
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 } ;
{ (y "/\" x) where x is Element of R : x in X } = { (x "/\" y) where x is Element of R : x in X }

proof

thus { (y "/\" x) where x is Element of R : x in X } c= { (x "/\" y) where x is Element of R : x in X } :: according to XBOOLE_0:def 10 :: thesis: { (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 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 consider x being Element of R such that
A2: z = y "/\" x and
A3: x in X ;
thus z in { (x "/\" y) where x is Element of R : x in X } by A2, A3; :: thesis: verum

end;

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

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 consider x being Element of R such that
A4: w = x "/\" y and
A5: x in X ;
thus w in { (y "/\" x) where x is Element of R : x in X } by A4, A5; :: thesis: verum

end;

end;

hence ("\/" X,R) "/\" y = "\/" { (x "/\" y) where x is Element of R : x in X } ,R by A1, WAYBEL_1:66; :: thesis: verum