let L be complete LATTICE; :: thesis: for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup

let J be non empty set ; :: thesis: for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup

let K be V9() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Inf >= Sup
let F be DoubleIndexedSet of K,L; :: thesis:
set a = Sup ;
A1: for j being Element of J
for f being Element of product (doms F) holds Sup >= Inf
proof
let j be Element of J; :: thesis: for f being Element of product (doms F) holds Sup >= Inf
let f be Element of product (doms F); :: thesis:
A2: f in dom () by Lm7;
then reconsider k = f . j as Element of K . j by Lm6;
(F . j) . k = (() . f) . j by ;
then A3: Inf <= (F . j) . k by YELLOW_2:53;
(F . j) . k <= Sup by YELLOW_2:53;
hence Sup >= Inf by ; :: thesis: verum
end;
Sup is_<=_than rng ()
proof
let c be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not c in rng () or Sup <= c )
assume c in rng () ; :: thesis:
then consider j being Element of J such that
A4: c = Sup by Th14;
for f being Function st f in dom () holds
//\ ((() . f),L) <= c by A1, A4;
hence Sup <= c by Th15; :: thesis: verum
end;
then Sup <= inf (rng ()) by YELLOW_0:33;
hence Inf >= Sup by YELLOW_2:def 6; :: thesis: verum