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 & (1,2 --> ({1} --> x),(id X)) . 2 = id X ) by FUNCT_4:66;
A2: ( (1,2 --> {1},X) . 1 = {1} & (1,2 --> {1},X) . 2 = X ) by FUNCT_4:66;
reconsider j1 = 1, j2 = 2 as Element of {1,2} by TARSKI:def 2;
dom (1,2 --> {1},X) = {1,2} by FUNCT_4:65;
then reconsider K = 1,2 --> {1},X as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
for i being set st i in {1,2} holds
not K . i is empty by A2, TARSKI:def 2;
then reconsider K = K as V9() ManySortedSet of by PBOOLE:def 16;
dom (1,2 --> ({1} --> x),(id X)) = {1,2} by FUNCT_4:65;
then reconsider F = 1,2 --> ({1} --> x),(id X) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
for j being set st j in {1,2} holds
F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)

proof

let j be set ; :: thesis: ( j in {1,2} implies F . j is Function of (K . j),(({1,2} --> the carrier of L) . j) )
assume A3: j in {1,2} ; :: thesis: F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
then A4: ({1,2} --> the carrier of L) . j = the carrier of L by FUNCOP_1:13;

per cases ( j = 1 or j = 2 ) by A3, TARSKI:def 2;

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 A1, A2, A4; :: 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 A1, A2, A4, FUNCT_2:9; :: thesis: verum

end;

end;

end;

then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def 18;
x "/\" (sup X) is_<=_than rng (Sups )

proof

let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in rng (Sups ) or x "/\" (sup X) <= y )
assume y in rng (Sups ) ; :: thesis: x "/\" (sup X) <= y
then consider j being Element of {1,2} such that
A5: y = Sup by Th14;

per cases ( j = 1 or j = 2 ) by TARSKI:def 2;

suppose j = 1 ; :: thesis: x "/\" (sup X) <= y

then rng (F . j) = {x} by A1, FUNCOP_1:14;
then Sup = sup {x} by YELLOW_2:def 5;
then y = x by A5, YELLOW_0:39;
hence x "/\" (sup X) <= y by YELLOW_0:23; :: thesis: verum

end;

suppose j = 2 ; :: thesis: x "/\" (sup X) <= y

then rng (F . j) = X by A1, RELAT_1:71;
then y = sup X by A5, YELLOW_2:def 5;
hence x "/\" (sup X) <= y by YELLOW_0:23; :: thesis: verum

end;

end;

end;

then x "/\" (sup X) <= inf (rng (Sups )) by YELLOW_0:33;
then x "/\" (sup X) <= Inf by YELLOW_2:def 6;
then A6: x "/\" (sup X) <= Sup by Def3;
rng (Infs ) 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 (Infs ) or y <= "\/" { (x "/\" y) where y is Element of L : y in X } ,L )
assume y in rng (Infs ) ; :: thesis: y <= "\/" { (x "/\" y) where y is Element of L : y in X } ,L
then consider f being set such that
A7: f in dom (Frege F) and
A8: y = //\ ((Frege F) . f),L by Th13;
reconsider f = f as Function by A7, Th7;
A9: ( f . j1 in K . j1 & f . j2 in K . j2 ) by A7, Lm6;
then reconsider f2 = f . 2 as Element of X by FUNCT_4:66;
A10: y = "/\" (rng ((Frege F) . f)),L by A8, YELLOW_2:def 6;
A11: ( ex_inf_of rng ((Frege F) . f),L & ex_inf_of {x,(f . 2)},L ) by YELLOW_0:17;
{x,f2} c= rng ((Frege F) . f)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,f2} or z in rng ((Frege F) . f) )
assume z in {x,f2} ; :: thesis: z in rng ((Frege F) . 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 A1, A2, A9, FUNCOP_1:13, FUNCT_1:35;
hence z in rng ((Frege F) . f) by A7, Lm5; :: thesis: verum

end;

then y <= inf {x,f2} by A10, A11, YELLOW_0:35;
then A12: y <= x "/\" f2 by YELLOW_0:40;
x "/\" f2 in { (x "/\" y) where y is Element of L : y in X } ;
then x "/\" f2 <= "\/" { (x "/\" y) where y is Element of L : y in X } ,L by YELLOW_2:24;
hence y <= "\/" { (x "/\" y) where y is Element of L : y in X } ,L by A12, YELLOW_0:def 2; :: thesis: verum

end;

then sup (rng (Infs )) <= "\/" { (x "/\" y) where y is Element of L : y in X } ,L by YELLOW_0:32;
then Sup <= "\/" { (x "/\" y) where y is Element of L : y in X } ,L by YELLOW_2:def 5;
then A13: x "/\" (sup X) <= "\/" { (x "/\" y) where y is Element of L : y in X } ,L by A6, YELLOW_0:def 2;
(x "/\" ) .: X = { (x "/\" y) where y is Element of L : y in X } by WAYBEL_1:64;
then reconsider A' = { (x "/\" y) where y is Element of L : y in X } as Subset of L ;
( ex_sup_of X,L & ex_sup_of A',L ) by YELLOW_0:17;
then x "/\" (sup X) >= sup A' by Th25;
hence x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of L : y in X } ,L by A13, YELLOW_0:def 3; :: thesis: verum