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;