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 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;
{ (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 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;
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, 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