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 A4, PARTFUN1:def 2, RELAT_1:def 18;

A6: ((1,2) --> ({1},X)) . 1 = {1} by FUNCT_4:63;

reconsider K = (1,2) --> ({1},X) as ManySortedSet of {1,2} by A2, PARTFUN1:def 2, RELAT_1:def 18;

for i being object st i in {1,2} holds

not K . i is empty by A6, A3, TARSKI:def 2;

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)

rng (Infs ) is_<=_than "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

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 (Sups )

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 A16, YELLOW_0:def 2;

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

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 A4, PARTFUN1:def 2, RELAT_1:def 18;

A6: ((1,2) --> ({1},X)) . 1 = {1} by FUNCT_4:63;

reconsider K = (1,2) --> ({1},X) as ManySortedSet of {1,2} by A2, PARTFUN1:def 2, RELAT_1:def 18;

for i being object st i in {1,2} holds

not K . i is empty by A6, A3, TARSKI:def 2;

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

then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def 15;
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;

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

rng (Infs ) is_<=_than "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)

proof

then
sup (rng (Infs )) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
by YELLOW_0:32;
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 object such that

A9: f in dom (Frege F) and

A10: y = //\ (((Frege F) . f),L) by Th13;

reconsider f = f as Function by A9;

A11: f . j2 in K . j2 by A9, Lm6;

then reconsider f2 = f . 2 as Element of X by FUNCT_4:63;

A12: f . j1 in K . j1 by A9, Lm6;

A13: {x,f2} c= rng ((Frege F) . f)

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 ((Frege F) . f),L & ex_inf_of {x,(f . 2)},L ) by YELLOW_0:17;

y = "/\" ((rng ((Frege F) . f)),L) by A10, YELLOW_2:def 6;

then y <= inf {x,f2} by A15, A13, YELLOW_0:35;

then y <= x "/\" f2 by YELLOW_0:40;

hence y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A14, YELLOW_0:def 2; :: thesis: verum

end;assume y in rng (Infs ) ; :: 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 (Frege F) and

A10: y = //\ (((Frege F) . f),L) by Th13;

reconsider f = f as Function by A9;

A11: f . j2 in K . j2 by A9, Lm6;

then reconsider f2 = f . 2 as Element of X by FUNCT_4:63;

A12: f . j1 in K . j1 by A9, Lm6;

A13: {x,f2} c= rng ((Frege F) . f)

proof

x "/\" f2 in { (x "/\" y) where y is Element of L : y in X }
;
let z be object ; :: 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, A5, A6, A3, A12, A11, FUNCOP_1:7, FUNCT_1:18;

hence z in rng ((Frege F) . f) by A9, Lm5; :: thesis: verum

end;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, A5, A6, A3, A12, A11, FUNCOP_1:7, FUNCT_1:18;

hence z in rng ((Frege F) . f) by A9, Lm5; :: thesis: verum

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 ((Frege F) . f),L & ex_inf_of {x,(f . 2)},L ) by YELLOW_0:17;

y = "/\" ((rng ((Frege F) . f)),L) by A10, YELLOW_2:def 6;

then y <= inf {x,f2} by A15, A13, YELLOW_0:35;

then y <= x "/\" f2 by YELLOW_0:40;

hence y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by A14, YELLOW_0:def 2; :: thesis: verum

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 (Sups )

proof

then
x "/\" (sup X) <= inf (rng (Sups ))
by YELLOW_0:33;
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

A18: y = Sup by Th14;

end;assume y in rng (Sups ) ; :: thesis: x "/\" (sup X) <= y

then consider j being Element of {1,2} such that

A18: y = Sup by Th14;

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 A16, YELLOW_0:def 2;

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