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 :: thesis: not { (x "/\" y) where y is Element of L : y in X } <> {}

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;

then A2: "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) = Bottom L by YELLOW_0:def 11;
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;

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;