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 }

( 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, YELLOW_0:17;

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

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

{ (y "/\" x) where x is Element of R : x in X } c= { (x "/\" y) where x is Element of R : x in X }
let w be object ; :: 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;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

proof

then
( ( for z being Element of R holds
let z be object ; :: 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;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

( 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, YELLOW_0:17;

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