let L be complete LATTICE; :: thesis: ( L is completely-distributive iff for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf )

thus ( L is completely-distributive implies for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf ) :: thesis: ( ( for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf ) implies L is completely-distributive )

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf ; :: thesis: L is completely-distributive

thus L is complete ; :: according to WAYBEL_5:def 3 :: thesis: for b_{1} being set

for b_{2} being set

for b_{3} being ManySortedFunction of b_{2},b_{1} --> the carrier of L holds //\ ((\// (b_{3},L)),L) = \\/ ((/\\ ((Frege b_{3}),L)),L)

let J be non empty set ; :: thesis: for b_{1} being set

for b_{2} being ManySortedFunction of b_{1},J --> the carrier of L holds //\ ((\// (b_{2},L)),L) = \\/ ((/\\ ((Frege b_{2}),L)),L)

let K be V8() ManySortedSet of J; :: thesis: for b_{1} being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b_{1},L)),L) = \\/ ((/\\ ((Frege b_{1}),L)),L)

let F be DoubleIndexedSet of K,L; :: thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)

A23: dom K = J by PARTFUN1:def 2;

A24: doms (Frege F) = (product (doms F)) --> J by Th45;

A25: dom F = J by PARTFUN1:def 2;

A26: doms F = K by Th45;

A27: dom (Frege F) = product (doms F) by PARTFUN1:def 2;

rng (Sups ) is_>=_than Inf

then A41: Inf >= Inf by YELLOW_2:def 6;

( Inf >= Sup & Sup = Inf ) by A22, WAYBEL_5:16;

hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) by A41, ORDERS_2:2; :: thesis: verum

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf )

thus ( L is completely-distributive implies for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf ) :: thesis: ( ( for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf ) implies L is completely-distributive )

proof

assume A22:
for J being non empty set
assume that

L is complete and

A1: for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: according to WAYBEL_5:def 3 :: thesis: for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf

let J be non empty set ; :: thesis: for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf

let K be V8() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Sup = Inf

let F be DoubleIndexedSet of K,L; :: thesis: Sup = Inf

A2: Inf = Sup by A1;

A3: dom K = J by PARTFUN1:def 2;

A4: doms (Frege F) = (product (doms F)) --> J by Th45;

A6: doms F = K by Th45;

rng (Infs ) is_<=_than Sup

then A21: Sup <= Sup by YELLOW_2:def 5;

Sup <= Inf by Th47;

hence Sup = Inf by A2, A21, ORDERS_2:2; :: thesis: verum

end;L is complete and

A1: for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: according to WAYBEL_5:def 3 :: thesis: for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf

let J be non empty set ; :: thesis: for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf

let K be V8() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Sup = Inf

let F be DoubleIndexedSet of K,L; :: thesis: Sup = Inf

A2: Inf = Sup by A1;

A3: dom K = J by PARTFUN1:def 2;

A4: doms (Frege F) = (product (doms F)) --> J by Th45;

A6: doms F = K by Th45;

rng (Infs ) is_<=_than Sup

proof

then
sup (rng (Infs )) <= Sup
by YELLOW_0:32;
reconsider J9 = product (doms (Frege F)) as non empty set ;

let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng (Infs ) or a <= Sup )

reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;

reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ;

assume a in rng (Infs ) ; :: thesis: a <= Sup

then consider g being Element of J9 such that

A8: a = Inf by WAYBEL_5:14;

reconsider g9 = g as Function ;

deffunc H_{1}( object ) -> set = { (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = $1 } ;

A9: dom ((product (doms F)) --> J) = product (doms F) ;

A13: (K . j) \ H_{1}(j) = {}
;

A14: rng (F . j) c= rng (G . g)

then inf (rng (G . g)) <= inf (rng (F . j)) by A14, YELLOW_0:35;

then a <= inf (rng (F . j)) by A8, YELLOW_2:def 6;

then A20: a <= Inf by YELLOW_2:def 6;

Inf in rng (Infs ) by WAYBEL_5:14;

then Inf <= sup (rng (Infs )) by YELLOW_2:22;

then a <= sup (rng (Infs )) by A20, ORDERS_2:3;

hence a <= Sup by YELLOW_2:def 5; :: thesis: verum

end;let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng (Infs ) or a <= Sup )

reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;

reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ;

assume a in rng (Infs ) ; :: thesis: a <= Sup

then consider g being Element of J9 such that

A8: a = Inf by WAYBEL_5:14;

reconsider g9 = g as Function ;

deffunc H

A9: dom ((product (doms F)) --> J) = product (doms F) ;

now :: thesis: not for j being Element of J holds (K . j) \ H_{1}(j) <> {}

then consider j being Element of J such that defpred S_{1}[ object , object ] means $2 in (K . $1) \ H_{1}($1);

assume A10: for j being Element of J holds (K . j) \ H_{1}(j) <> {}
; :: thesis: contradiction

A12: ( dom h = J & ( for j being object st j in J holds

S_{1}[j,h . j] ) )
from CLASSES1:sch 1(A11);

g9 . h in (doms (Frege F)) . h by A4, A9, CARD_3:9;

then reconsider j = g9 . h as Element of J by A4;

( h . (g9 . h) in H_{1}(j) & h . j in (K . j) \ H_{1}(j) )
by A12;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;assume A10: for j being Element of J holds (K . j) \ H

A11: now :: thesis: for j being object st j in J holds

ex k being object st S_{1}[j,k]

consider h being Function such that ex k being object st S

let j be object ; :: thesis: ( j in J implies ex k being object st S_{1}[j,k] )

assume j in J ; :: thesis: ex k being object st S_{1}[j,k]

then reconsider i = j as Element of J ;

set k = the Element of (K . i) \ H_{1}(j);

(K . i) \ H_{1}(i) <> {}
by A10;

then the Element of (K . i) \ H_{1}(j) in (K . i) \ H_{1}(i)
;

hence ex k being object st S_{1}[j,k]
; :: thesis: verum

end;assume j in J ; :: thesis: ex k being object st S

then reconsider i = j as Element of J ;

set k = the Element of (K . i) \ H

(K . i) \ H

then the Element of (K . i) \ H

hence ex k being object st S

A12: ( dom h = J & ( for j being object st j in J holds

S

now :: thesis: for j being object st j in J holds

h . j in (doms F) . j

then reconsider h = h as Element of product (doms F) by A6, A3, A12, CARD_3:9;h . j in (doms F) . j

let j be object ; :: thesis: ( j in J implies h . j in (doms F) . j )

assume j in J ; :: thesis: h . j in (doms F) . j

then h . j in (K . j) \ H_{1}(j)
by A12;

hence h . j in (doms F) . j by A6; :: thesis: verum

end;assume j in J ; :: thesis: h . j in (doms F) . j

then h . j in (K . j) \ H

hence h . j in (doms F) . j by A6; :: thesis: verum

g9 . h in (doms (Frege F)) . h by A4, A9, CARD_3:9;

then reconsider j = g9 . h as Element of J by A4;

( h . (g9 . h) in H

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

A13: (K . j) \ H

A14: rng (F . j) c= rng (G . g)

proof

( ex_inf_of rng (G . g),L & ex_inf_of rng (F . j),L )
by YELLOW_0:17;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (F . j) or z in rng (G . g) )

assume z in rng (F . j) ; :: thesis: z in rng (G . g)

then consider u being object such that

A15: u in dom (F . j) and

A16: z = (F . j) . u by FUNCT_1:def 3;

reconsider u = u as Element of K . j by A15;

u in H_{1}(j)
by A13, XBOOLE_0:def 5;

then consider f being Element of product (doms F) such that

A17: u = f . (g9 . f) and

A18: g9 . f = j ;

A: ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def 2;

consider gg being Function such that

BB: ( f = gg & dom gg = dom (doms F) & ( for y being object st y in dom (doms F) holds

gg . y in (doms F) . y ) ) by CARD_3:def 5;

A25: dom F = J by PARTFUN1:def 2;

BC: dom f = dom F by FUNCT_6:def 2, BB;

j in (dom F) /\ (dom f) by A25, BC;

then j in dom (F .. f) by PRALG_1:def 19;

then WW: (F .. f) . j = (F . j) . (f . j) by PRALG_1:def 19;

A27: dom (Frege F) = product (doms F) by PARTFUN1:def 2;

consider gg1 being Function such that

BB: ( g = gg1 & dom gg1 = dom (doms (Frege F)) & ( for y being object st y in dom (doms (Frege F)) holds

gg1 . y in (doms (Frege F)) . y ) ) by CARD_3:def 5;

f in dom (Frege F) by A27;

then f in dom (doms (Frege F)) by FUNCT_6:def 2;

then f in (dom (Frege F)) /\ (dom g9) by A27, BB, XBOOLE_0:def 4;

then f in dom ((Frege F) .. g9) by PRALG_1:def 19;

then (G . g) . f = (F .. f) . j by A18, PRALG_1:def 19, A;

then A19: (G . g) . f = z by A16, A17, A18, WW;

( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCT_2:def 1;

hence z in rng (G . g) by A19, FUNCT_1:def 3; :: thesis: verum

end;assume z in rng (F . j) ; :: thesis: z in rng (G . g)

then consider u being object such that

A15: u in dom (F . j) and

A16: z = (F . j) . u by FUNCT_1:def 3;

reconsider u = u as Element of K . j by A15;

u in H

then consider f being Element of product (doms F) such that

A17: u = f . (g9 . f) and

A18: g9 . f = j ;

A: ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def 2;

consider gg being Function such that

BB: ( f = gg & dom gg = dom (doms F) & ( for y being object st y in dom (doms F) holds

gg . y in (doms F) . y ) ) by CARD_3:def 5;

A25: dom F = J by PARTFUN1:def 2;

BC: dom f = dom F by FUNCT_6:def 2, BB;

j in (dom F) /\ (dom f) by A25, BC;

then j in dom (F .. f) by PRALG_1:def 19;

then WW: (F .. f) . j = (F . j) . (f . j) by PRALG_1:def 19;

A27: dom (Frege F) = product (doms F) by PARTFUN1:def 2;

consider gg1 being Function such that

BB: ( g = gg1 & dom gg1 = dom (doms (Frege F)) & ( for y being object st y in dom (doms (Frege F)) holds

gg1 . y in (doms (Frege F)) . y ) ) by CARD_3:def 5;

f in dom (Frege F) by A27;

then f in dom (doms (Frege F)) by FUNCT_6:def 2;

then f in (dom (Frege F)) /\ (dom g9) by A27, BB, XBOOLE_0:def 4;

then f in dom ((Frege F) .. g9) by PRALG_1:def 19;

then (G . g) . f = (F .. f) . j by A18, PRALG_1:def 19, A;

then A19: (G . g) . f = z by A16, A17, A18, WW;

( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCT_2:def 1;

hence z in rng (G . g) by A19, FUNCT_1:def 3; :: thesis: verum

then inf (rng (G . g)) <= inf (rng (F . j)) by A14, YELLOW_0:35;

then a <= inf (rng (F . j)) by A8, YELLOW_2:def 6;

then A20: a <= Inf by YELLOW_2:def 6;

Inf in rng (Infs ) by WAYBEL_5:14;

then Inf <= sup (rng (Infs )) by YELLOW_2:22;

then a <= sup (rng (Infs )) by A20, ORDERS_2:3;

hence a <= Sup by YELLOW_2:def 5; :: thesis: verum

then A21: Sup <= Sup by YELLOW_2:def 5;

Sup <= Inf by Th47;

hence Sup = Inf by A2, A21, ORDERS_2:2; :: thesis: verum

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup = Inf ; :: thesis: L is completely-distributive

thus L is complete ; :: according to WAYBEL_5:def 3 :: thesis: for b

for b

for b

let J be non empty set ; :: thesis: for b

for b

let K be V8() ManySortedSet of J; :: thesis: for b

let F be DoubleIndexedSet of K,L; :: thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)

A23: dom K = J by PARTFUN1:def 2;

A24: doms (Frege F) = (product (doms F)) --> J by Th45;

A25: dom F = J by PARTFUN1:def 2;

A26: doms F = K by Th45;

A27: dom (Frege F) = product (doms F) by PARTFUN1:def 2;

rng (Sups ) is_>=_than Inf

proof

then
inf (rng (Sups )) >= Inf
by YELLOW_0:33;
reconsider J9 = product (doms (Frege F)) as non empty set ;

let a be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not a in rng (Sups ) or Inf <= a )

reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;

reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ;

assume a in rng (Sups ) ; :: thesis: Inf <= a

then consider g being Element of J9 such that

A28: a = Sup by WAYBEL_5:14;

reconsider g9 = g as Function ;

deffunc H_{1}( object ) -> set = { (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = $1 } ;

A29: dom ((product (doms F)) --> J) = product (doms F) ;

A33: (K . j) \ H_{1}(j) = {}
;

A34: rng (F . j) c= rng (G . g)

then sup (rng (G . g)) >= sup (rng (F . j)) by A34, YELLOW_0:34;

then a >= sup (rng (F . j)) by A28, YELLOW_2:def 5;

then A40: a >= Sup by YELLOW_2:def 5;

Sup in rng (Sups ) by WAYBEL_5:14;

then Sup >= inf (rng (Sups )) by YELLOW_2:22;

then a >= inf (rng (Sups )) by A40, ORDERS_2:3;

hence Inf <= a by YELLOW_2:def 6; :: thesis: verum

end;let a be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not a in rng (Sups ) or Inf <= a )

reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;

reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ;

assume a in rng (Sups ) ; :: thesis: Inf <= a

then consider g being Element of J9 such that

A28: a = Sup by WAYBEL_5:14;

reconsider g9 = g as Function ;

deffunc H

A29: dom ((product (doms F)) --> J) = product (doms F) ;

now :: thesis: not for j being Element of J holds (K . j) \ H_{1}(j) <> {}

then consider j being Element of J such that defpred S_{1}[ object , object ] means $2 in (K . $1) \ H_{1}($1);

assume A30: for j being Element of J holds (K . j) \ H_{1}(j) <> {}
; :: thesis: contradiction

A32: ( dom h = J & ( for j being object st j in J holds

S_{1}[j,h . j] ) )
from CLASSES1:sch 1(A31);

g9 . h in (doms (Frege F)) . h by A24, A29, CARD_3:9;

then reconsider j = g9 . h as Element of J by A24;

( h . (g9 . h) in H_{1}(j) & h . j in (K . j) \ H_{1}(j) )
by A32;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;assume A30: for j being Element of J holds (K . j) \ H

A31: now :: thesis: for j being object st j in J holds

ex k being object st S_{1}[j,k]

consider h being Function such that ex k being object st S

let j be object ; :: thesis: ( j in J implies ex k being object st S_{1}[j,k] )

assume j in J ; :: thesis: ex k being object st S_{1}[j,k]

then reconsider i = j as Element of J ;

set k = the Element of (K . i) \ H_{1}(j);

(K . i) \ H_{1}(i) <> {}
by A30;

then the Element of (K . i) \ H_{1}(j) in (K . i) \ H_{1}(i)
;

hence ex k being object st S_{1}[j,k]
; :: thesis: verum

end;assume j in J ; :: thesis: ex k being object st S

then reconsider i = j as Element of J ;

set k = the Element of (K . i) \ H

(K . i) \ H

then the Element of (K . i) \ H

hence ex k being object st S

A32: ( dom h = J & ( for j being object st j in J holds

S

now :: thesis: for j being object st j in J holds

h . j in (doms F) . j

then reconsider h = h as Element of product (doms F) by A26, A23, A32, CARD_3:9;h . j in (doms F) . j

let j be object ; :: thesis: ( j in J implies h . j in (doms F) . j )

assume j in J ; :: thesis: h . j in (doms F) . j

then h . j in (K . j) \ H_{1}(j)
by A32;

hence h . j in (doms F) . j by A26; :: thesis: verum

end;assume j in J ; :: thesis: h . j in (doms F) . j

then h . j in (K . j) \ H

hence h . j in (doms F) . j by A26; :: thesis: verum

g9 . h in (doms (Frege F)) . h by A24, A29, CARD_3:9;

then reconsider j = g9 . h as Element of J by A24;

( h . (g9 . h) in H

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

A33: (K . j) \ H

A34: rng (F . j) c= rng (G . g)

proof

( ex_sup_of rng (G . g),L & ex_sup_of rng (F . j),L )
by YELLOW_0:17;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (F . j) or z in rng (G . g) )

assume z in rng (F . j) ; :: thesis: z in rng (G . g)

then consider u being object such that

A35: u in dom (F . j) and

A36: z = (F . j) . u by FUNCT_1:def 3;

reconsider u = u as Element of K . j by A35;

u in H_{1}(j)
by A33, XBOOLE_0:def 5;

then consider f being Element of product (doms F) such that

A37: u = f . (g9 . f) and

A38: g9 . f = j ;

a37: ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def 2;

consider gg being Function such that

BB: ( f = gg & dom gg = dom (doms F) & ( for y being object st y in dom (doms F) holds

gg . y in (doms F) . y ) ) by CARD_3:def 5;

dom F = dom f by BB, FUNCT_6:def 2;

then j in (dom F) /\ (dom f) by A25;

then Z1: j in dom (F .. f) by PRALG_1:def 19;

consider gg1 being Function such that

BB: ( g = gg1 & dom gg1 = dom (doms (Frege F)) & ( for y being object st y in dom (doms (Frege F)) holds

gg1 . y in (doms (Frege F)) . y ) ) by CARD_3:def 5;

f in dom (Frege F) by A27;

then f in dom g9 by BB, FUNCT_6:def 2;

then f in (dom (Frege F)) /\ (dom g9) by A27, XBOOLE_0:def 4;

then a38: f in dom ((Frege F) .. g9) by PRALG_1:def 19;

(G . g) . f = ((Frege F) . f) . (g9 . f) by a37, a38, PRALG_1:def 19;

then A39: (G . g) . f = z by Z1, A36, a37, A37, A38, PRALG_1:def 19;

( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCT_2:def 1;

hence z in rng (G . g) by A39, FUNCT_1:def 3; :: thesis: verum

end;assume z in rng (F . j) ; :: thesis: z in rng (G . g)

then consider u being object such that

A35: u in dom (F . j) and

A36: z = (F . j) . u by FUNCT_1:def 3;

reconsider u = u as Element of K . j by A35;

u in H

then consider f being Element of product (doms F) such that

A37: u = f . (g9 . f) and

A38: g9 . f = j ;

a37: ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def 2;

consider gg being Function such that

BB: ( f = gg & dom gg = dom (doms F) & ( for y being object st y in dom (doms F) holds

gg . y in (doms F) . y ) ) by CARD_3:def 5;

dom F = dom f by BB, FUNCT_6:def 2;

then j in (dom F) /\ (dom f) by A25;

then Z1: j in dom (F .. f) by PRALG_1:def 19;

consider gg1 being Function such that

BB: ( g = gg1 & dom gg1 = dom (doms (Frege F)) & ( for y being object st y in dom (doms (Frege F)) holds

gg1 . y in (doms (Frege F)) . y ) ) by CARD_3:def 5;

f in dom (Frege F) by A27;

then f in dom g9 by BB, FUNCT_6:def 2;

then f in (dom (Frege F)) /\ (dom g9) by A27, XBOOLE_0:def 4;

then a38: f in dom ((Frege F) .. g9) by PRALG_1:def 19;

(G . g) . f = ((Frege F) . f) . (g9 . f) by a37, a38, PRALG_1:def 19;

then A39: (G . g) . f = z by Z1, A36, a37, A37, A38, PRALG_1:def 19;

( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCT_2:def 1;

hence z in rng (G . g) by A39, FUNCT_1:def 3; :: thesis: verum

then sup (rng (G . g)) >= sup (rng (F . j)) by A34, YELLOW_0:34;

then a >= sup (rng (F . j)) by A28, YELLOW_2:def 5;

then A40: a >= Sup by YELLOW_2:def 5;

Sup in rng (Sups ) by WAYBEL_5:14;

then Sup >= inf (rng (Sups )) by YELLOW_2:22;

then a >= inf (rng (Sups )) by A40, ORDERS_2:3;

hence Inf <= a by YELLOW_2:def 6; :: thesis: verum

then A41: Inf >= Inf by YELLOW_2:def 6;

( Inf >= Sup & Sup = Inf ) by A22, WAYBEL_5:16;

hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) by A41, ORDERS_2:2; :: thesis: verum