let L be complete LATTICE; :: thesis: for J, K being non empty set

for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf >= sup X

let J, K be non empty set ; :: thesis: for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf >= sup X

let F be Function of [:J,K:], the carrier of L; :: thesis: for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf >= sup X

let X be Subset of L; :: thesis: ( X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } implies Inf >= sup X )

A1: for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

for j being Element of J holds Sup >= Sup

for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

Inf >= Inf

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } ; :: thesis: Inf >= sup X

Inf is_>=_than X

for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf >= sup X

let J, K be non empty set ; :: thesis: for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf >= sup X

let F be Function of [:J,K:], the carrier of L; :: thesis: for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf >= sup X

let X be Subset of L; :: thesis: ( X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } implies Inf >= sup X )

A1: for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

for j being Element of J holds Sup >= Sup

proof

A5:
for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds
let f be V9() ManySortedSet of J; :: thesis: ( f in Funcs (J,(Fin K)) implies for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

for j being Element of J holds Sup >= Sup )

assume A2: f in Funcs (J,(Fin K)) ; :: thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

for j being Element of J holds Sup >= Sup

let G be DoubleIndexedSet of f,L; :: thesis: ( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) implies for j being Element of J holds Sup >= Sup )

assume A3: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ; :: thesis: for j being Element of J holds Sup >= Sup

let j be Element of J; :: thesis: Sup >= Sup

A4: ( ex_sup_of rng ((curry F) . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17;

rng (G . j) is Subset of (rng ((curry F) . j)) by A2, A3, Lm12;

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

then Sup >= sup (rng (G . j)) by YELLOW_2:def 5;

hence Sup >= Sup by YELLOW_2:def 5; :: thesis: verum

end;for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

for j being Element of J holds Sup >= Sup )

assume A2: f in Funcs (J,(Fin K)) ; :: thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

for j being Element of J holds Sup >= Sup

let G be DoubleIndexedSet of f,L; :: thesis: ( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) implies for j being Element of J holds Sup >= Sup )

assume A3: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ; :: thesis: for j being Element of J holds Sup >= Sup

let j be Element of J; :: thesis: Sup >= Sup

A4: ( ex_sup_of rng ((curry F) . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17;

rng (G . j) is Subset of (rng ((curry F) . j)) by A2, A3, Lm12;

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

then Sup >= sup (rng (G . j)) by YELLOW_2:def 5;

hence Sup >= Sup by YELLOW_2:def 5; :: thesis: verum

for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

Inf >= Inf

proof

assume A10:
X = { a where a is Element of L : ex f being V9() ManySortedSet of J st
let f be V9() ManySortedSet of J; :: thesis: ( f in Funcs (J,(Fin K)) implies for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

Inf >= Inf )

assume A6: f in Funcs (J,(Fin K)) ; :: thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

Inf >= Inf

let G be DoubleIndexedSet of f,L; :: thesis: ( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) implies Inf >= Inf )

assume A7: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ; :: thesis: Inf >= Inf

rng (Sups ) is_>=_than Inf

hence Inf >= Inf by YELLOW_2:def 6; :: thesis: verum

end;for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

Inf >= Inf )

assume A6: f in Funcs (J,(Fin K)) ; :: thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) holds

Inf >= Inf

let G be DoubleIndexedSet of f,L; :: thesis: ( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) implies Inf >= Inf )

assume A7: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ; :: thesis: Inf >= Inf

rng (Sups ) is_>=_than Inf

proof

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

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

then consider j being Element of J such that

A8: a = Sup by Th14;

Sup in rng (Sups ) by Th14;

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

then A9: Sup >= Inf by YELLOW_2:def 6;

Sup >= Sup by A1, A6, A7;

hence Inf <= a by A8, A9, ORDERS_2:3; :: thesis: verum

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

then consider j being Element of J such that

A8: a = Sup by Th14;

Sup in rng (Sups ) by Th14;

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

then A9: Sup >= Inf by YELLOW_2:def 6;

Sup >= Sup by A1, A6, A7;

hence Inf <= a by A8, A9, ORDERS_2:3; :: thesis: verum

hence Inf >= Inf by YELLOW_2:def 6; :: thesis: verum

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } ; :: thesis: Inf >= sup X

Inf is_>=_than X

proof

hence
Inf >= sup X
by YELLOW_0:32; :: thesis: verum
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in X or a <= Inf )

assume a in X ; :: thesis: a <= Inf

then ex a9 being Element of L st

( a9 = a & ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a9 = Inf ) ) ) by A10;

hence a <= Inf by A5; :: thesis: verum

end;assume a in X ; :: thesis: a <= Inf

then ex a9 being Element of L st

( a9 = a & ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a9 = Inf ) ) ) by A10;

hence a <= Inf by A5; :: thesis: verum