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 non-empty 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 non-empty 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 non-empty 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 non-empty 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 non-empty 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

let f be non-empty 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;

A5: for f being non-empty 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
Inf >= Inf

proof

let f be non-empty 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

proof

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;

then inf (rng (Sups )) >= Inf by YELLOW_0:33;
hence Inf >= Inf by YELLOW_2:def 6; :: thesis: verum

end;

assume A10: X = { a where a is Element of L : ex f being non-empty 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 ) ) } ; :: thesis: Inf >= sup X
Inf is_>=_than X

proof

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 non-empty 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;

hence Inf >= sup X by YELLOW_0:32; :: thesis: verum