let L be completely-distributive LATTICE; :: thesis: for X being Subset of L

for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

let X be Subset of L; :: thesis: for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

let x be Element of L; :: thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

set A = { (x "/\" y) where y is Element of L : y in X } ;

for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

let X be Subset of L; :: thesis: for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

let x be Element of L; :: thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

set A = { (x "/\" y) where y is Element of L : y in X } ;

per cases
( X is empty or not X is empty )
;

end;

suppose A1:
X is empty
; :: thesis: x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

sup X = Bottom L by A1, YELLOW_0:def 11;

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

end;

now :: thesis: not { (x "/\" y) where y is Element of L : y in X } <> {}

then A2:
"\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) = Bottom L
by YELLOW_0:def 11;set z = the Element of { (x "/\" y) where y is Element of L : y in X } ;

assume { (x "/\" y) where y is Element of L : y in X } <> {} ; :: thesis: contradiction

then the Element of { (x "/\" y) where y is Element of L : y in X } in { (x "/\" y) where y is Element of L : y in X } ;

then ex y being Element of L st

( the Element of { (x "/\" y) where y is Element of L : y in X } = x "/\" y & y in X ) ;

hence contradiction by A1; :: thesis: verum

end;assume { (x "/\" y) where y is Element of L : y in X } <> {} ; :: thesis: contradiction

then the Element of { (x "/\" y) where y is Element of L : y in X } in { (x "/\" y) where y is Element of L : y in X } ;

then ex y being Element of L st

( the Element of { (x "/\" y) where y is Element of L : y in X } = x "/\" y & y in X ) ;

hence contradiction by A1; :: thesis: verum

sup X = Bottom L by A1, YELLOW_0:def 11;

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