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 st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set 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 st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set 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 st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set 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 st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) & a = Inf ) ) } implies Inf >= sup X )
assume A1: X = { a where a is Element of L : ex f being V9() ManySortedSet of st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) & a = Inf ) ) } ; :: thesis: Inf >= sup X
A2: for f being V9() ManySortedSet of 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 set 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 V9() ManySortedSet of ; :: 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
for j being Element of J holds Sup >= Sup )
assume A3: f in Funcs J,(Fin K) ; :: thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J
for x being set 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 set st x in f . j holds
(G . j) . x = F . j,x ) implies for j being Element of J holds Sup >= Sup )
assume A4: for j being Element of J
for x being set 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
A5: ( 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 A3, A4, Lm12;
then sup (rng ((curry F) . j)) >= sup (rng (G . j)) by A5, 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;

A6: for f being V9() ManySortedSet of 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
Inf >= Inf

proof

let f be V9() ManySortedSet of ; :: 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
Inf >= Inf )
assume A7: f in Funcs J,(Fin K) ; :: thesis: for G being DoubleIndexedSet of f,L st ( for j being Element of J
for x being set 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 set st x in f . j holds
(G . j) . x = F . j,x ) implies Inf >= Inf )
assume A8: for j being Element of J
for x being set 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
A9: a = Sup by Th14;
A10: Sup >= Sup by A2, A7, A8;
Sup in rng (Sups ) by Th14;
then Sup >= inf (rng (Sups )) by YELLOW_2:24;
then Sup >= Inf by YELLOW_2:def 6;
hence Inf <= a by A9, A10, ORDERS_2:26; :: thesis: verum

end;

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

end;

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 consider a' being Element of L such that
A11: a' = a and
A12: ex f being V9() ManySortedSet of st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) & a' = Inf ) ) by A1;
consider f being V9() ManySortedSet of such that
A13: f in Funcs J,(Fin K) and
A14: ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) & a' = Inf ) by A12;
consider G being DoubleIndexedSet of f,L such that
A15: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x and
A16: a' = Inf by A14;
thus a <= Inf by A6, A11, A13, A15, A16; :: thesis: verum

end;

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