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 Sup <= Inf
let J be non empty set ; :: thesis: for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup <= Inf
let K be non-empty ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Sup <= Inf
let F be DoubleIndexedSet of K,L; :: thesis: Sup <= Inf
Inf is_>=_than rng (Infs )

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in rng (Infs ) or x <= Inf )
assume x in rng (Infs ) ; :: thesis: x <= Inf
then consider a being Element of J such that
A1: x = Inf by WAYBEL_5:14;
A2: x = inf (rng (F . a)) by A1, YELLOW_2:def 6;
x is_<=_than rng (Sups )

proof

reconsider J9 = product (doms F) as non empty set ;
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in rng (Sups ) or x <= y )
reconsider K9 = J9 --> J as ManySortedSet of J9 ;
reconsider G = Frege F as DoubleIndexedSet of K9,L ;
assume y in rng (Sups ) ; :: thesis: x <= y
then consider f being Element of J9 such that
A3: y = Sup by WAYBEL_5:14;
reconsider f = f as Element of product (doms F) ;
A4: ( dom F = J & dom (Frege F) = product (doms F) ) by PARTFUN1:def 2;
then f . a in dom (F . a) by WAYBEL_5:9;
then reconsider j = f . a as Element of K . a ;
A5: (F . a) . j in rng ((Frege F) . f) by A4, WAYBEL_5:9;
j in dom (F . a) by A4, WAYBEL_5:9;
then (F . a) . j in rng (F . a) by FUNCT_1:def 3;
then A6: x <= (F . a) . j by A2, YELLOW_2:22;
y = sup (rng ((Frege F) . f)) by A3, YELLOW_2:def 5;
then (F . a) . j <= y by A5, YELLOW_2:22;
hence x <= y by A6, ORDERS_2:3; :: thesis: verum

end;

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

end;

then sup (rng (Infs )) <= Inf by YELLOW_0:32;
hence Sup <= Inf by YELLOW_2:def 5; :: thesis: verum