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: Inf >= Sup

set a = Sup ;

A1: for j being Element of J

for f being Element of product (doms F) holds Sup >= Inf

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

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: Inf >= Sup

set a = Sup ;

A1: for j being Element of J

for f being Element of product (doms F) holds Sup >= Inf

proof

Sup is_<=_than rng (Sups )
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;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

proof

then
Sup <= inf (rng (Sups ))
by YELLOW_0:33;
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;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

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