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 } ;

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

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

now

assume A2: { (x "/\" y) where y is Element of L : y in X } <> {} ; :: thesis: contradiction
consider z being Element of { (x "/\" y) where y is Element of L : y in X } ;
z in { (x "/\" y) where y is Element of L : y in X } by A2;
then consider y being Element of L such that
A3: ( z = x "/\" y & y in X ) ;
thus contradiction by A1, A3; :: thesis: verum

end;

then ( sup X = Bottom L & "\/" { (x "/\" y) where y is Element of L : y in X } ,L = 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 WAYBEL_1:4; :: thesis: verum

end;

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

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

end;

end;