let L be complete LATTICE; :: thesis: for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup
let J be non empty set ; :: thesis: for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup
let K be non-empty ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Inf >= Sup
let F be DoubleIndexedSet of K,L; :: thesis: Inf >= Sup
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: Sup >= Inf
A2: f in dom (Frege F) by Lm7;
then reconsider k = f . j as Element of K . j by Lm6;
(F . j) . k = ((Frege F) . f) . j by A2, Lm5;
then A3: Inf <= (F . j) . k by YELLOW_2:53;
(F . j) . k <= Sup by YELLOW_2:53;
hence Sup >= Inf by A3, ORDERS_2:3; :: thesis: verum

end;

Sup is_<=_than rng (Sups )

proof

let c be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not c in rng (Sups ) or Sup <= c )
assume c in rng (Sups ) ; :: thesis: Sup <= c
then consider j being Element of J such that
A4: c = Sup by Th14;
for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= c by A1, A4;
hence Sup <= c by Th15; :: thesis: verum

end;

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