let L be completely-distributive LATTICE; :: thesis: for X being non empty 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 non empty 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 } ;
set J = {1,2};
set K = (1,2) --> ({1},X);
set F = (1,2) --> (({1} --> x),(id X));
A1: ((1,2) --> (({1} --> x),(id X))) . 1 = {1} --> x by FUNCT_4:63;
A2: dom ((1,2) --> ({1},X)) = {1,2} by FUNCT_4:62;
A3: ((1,2) --> ({1},X)) . 2 = X by FUNCT_4:63;
A4: dom ((1,2) --> (({1} --> x),(id X))) = {1,2} by FUNCT_4:62;
reconsider j1 = 1, j2 = 2 as Element of {1,2} by TARSKI:def 2;
A5: ((1,2) --> (({1} --> x),(id X))) . 2 = id X by FUNCT_4:63;
reconsider F = (1,2) --> (({1} --> x),(id X)) as ManySortedSet of {1,2} by ;
A6: ((1,2) --> ({1},X)) . 1 = {1} by FUNCT_4:63;
reconsider K = (1,2) --> ({1},X) as ManySortedSet of {1,2} by ;
for i being object st i in {1,2} holds
not K . i is empty by ;
then reconsider K = K as V9() ManySortedSet of {1,2} by PBOOLE:def 13;
for j being object st j in {1,2} holds
F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
proof
let j be object ; :: thesis: ( j in {1,2} implies F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) )
assume A7: j in {1,2} ; :: thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
then A8: ({1,2} --> the carrier of L) . j = the carrier of L by FUNCOP_1:7;
per cases ( j = 1 or j = 2 ) by ;
suppose j = 1 ; :: thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
hence F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) by ; :: thesis: verum
end;
suppose j = 2 ; :: thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
hence F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) by ; :: thesis: verum
end;
end;
end;
then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def 15;
rng () is_<=_than "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
proof
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in rng () or y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) )
assume y in rng () ; :: thesis: y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
then consider f being object such that
A9: f in dom () and
A10: y = //\ ((() . f),L) by Th13;
reconsider f = f as Function by A9;
A11: f . j2 in K . j2 by ;
then reconsider f2 = f . 2 as Element of X by FUNCT_4:63;
A12: f . j1 in K . j1 by ;
A13: {x,f2} c= rng (() . f)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,f2} or z in rng (() . f) )
assume z in {x,f2} ; :: thesis: z in rng (() . f)
then ( z = x or z = f . 2 ) by TARSKI:def 2;
then ( z = (F . j1) . (f . j1) or z = (F . j2) . (f . j2) ) by ;
hence z in rng (() . f) by ; :: thesis: verum
end;
x "/\" f2 in { (x "/\" y) where y is Element of L : y in X } ;
then A14: x "/\" f2 <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_2:22;
A15: ( ex_inf_of rng (() . f),L & ex_inf_of {x,(f . 2)},L ) by YELLOW_0:17;
y = "/\" ((rng (() . f)),L) by ;
then y <= inf {x,f2} by ;
then y <= x "/\" f2 by YELLOW_0:40;
hence y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by ; :: thesis: verum
end;
then sup (rng ()) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_0:32;
then A16: Sup <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by YELLOW_2:def 5;
(x "/\") .: X = { (x "/\" y) where y is Element of L : y in X } by WAYBEL_1:61;
then reconsider A9 = { (x "/\" y) where y is Element of L : y in X } as Subset of L ;
( ex_sup_of X,L & ex_sup_of A9,L ) by YELLOW_0:17;
then A17: x "/\" (sup X) >= sup A9 by Th25;
x "/\" (sup X) is_<=_than rng ()
proof
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in rng () or x "/\" (sup X) <= y )
assume y in rng () ; :: thesis: x "/\" (sup X) <= y
then consider j being Element of {1,2} such that
A18: y = Sup by Th14;
per cases ( j = 1 or j = 2 ) by TARSKI:def 2;
suppose j = 2 ; :: thesis: x "/\" (sup X) <= y
then rng (F . j) = X by A5;
then y = sup X by ;
hence x "/\" (sup X) <= y by YELLOW_0:23; :: thesis: verum
end;
end;
end;
then x "/\" (sup X) <= inf (rng ()) by YELLOW_0:33;
then x "/\" (sup X) <= Inf by YELLOW_2:def 6;
then x "/\" (sup X) <= Sup by Def3;
then x "/\" (sup X) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by ;
hence x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by ; :: thesis: verum