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

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

let K be V8() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Sup <= Inf
let F be DoubleIndexedSet of K,L; :: thesis:
Inf is_>=_than rng ()
proof
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in rng () or x <= Inf )
assume x in rng () ; :: thesis:
then consider a being Element of J such that
A1: x = Inf by WAYBEL_5:14;
A2: x = inf (rng (F . a)) by ;
x is_<=_than rng ()
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 () or x <= y )
reconsider K9 = J9 --> J as ManySortedSet of J9 ;
reconsider G = Frege F as DoubleIndexedSet of K9,L ;
assume y in rng () ; :: 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 () = 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 (() . f) by ;
j in dom (F . a) by ;
then (F . a) . j in rng (F . a) by FUNCT_1:def 3;
then A6: x <= (F . a) . j by ;
y = sup (rng (() . f)) by ;
then (F . a) . j <= y by ;
hence x <= y by ; :: thesis: verum
end;
then x <= inf (rng ()) by YELLOW_0:33;
hence x <= Inf by YELLOW_2:def 6; :: thesis: verum
end;
then sup (rng ()) <= Inf by YELLOW_0:32;
hence Sup <= Inf by YELLOW_2:def 5; :: thesis: verum