let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of
for X being Subset of (product J) holds
( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi X,i,J . i )
let J be non-Empty Poset-yielding ManySortedSet of ; :: thesis: for X being Subset of (product J) holds
( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi X,i,J . i )
let X be Subset of (product J); :: thesis: ( ex_inf_of X, product J iff for i being Element of I holds ex_inf_of pi X,i,J . i )

hereby :: thesis: ( ( for i being Element of I holds ex_inf_of pi X,i,J . i ) implies ex_inf_of X, product J )

assume A1: ex_inf_of X, product J ; :: thesis: for i being Element of I holds ex_inf_of pi X,i,J . i
let i be Element of I; :: thesis: ex_inf_of pi X,i,J . i
set f = inf X;
A2: inf X is_<=_than X by A1, YELLOW_0:31;
then A3: (inf X) . i is_<=_than pi X,i by Th32;

now

let x be Element of (J . i); :: thesis: ( pi X,i is_>=_than x implies (inf X) . i >= x )
assume A4: pi X,i is_>=_than x ; :: thesis: (inf X) . i >= x
set g = (inf X) +* i,x;
A5: ( dom ((inf X) +* i,x) = dom (inf X) & dom (inf X) = I ) by FUNCT_7:32, WAYBEL_3:27;
then A6: ((inf X) +* i,x) . i = x by FUNCT_7:33;

now

let j be Element of I; :: thesis: ((inf X) +* i,x) . j is Element of (J . j)
( ((inf X) +* i,x) . j = (inf X) . j or ( ((inf X) +* i,x) . j = x & j = i ) ) by A6, FUNCT_7:34;
hence ((inf X) +* i,x) . j is Element of (J . j) ; :: thesis: verum

end;

then reconsider g = (inf X) +* i,x as Element of (product J) by A5, WAYBEL_3:27;
X is_>=_than g

proof

let h be Element of (product J); :: according to LATTICE3:def 8 :: thesis: ( not h in X or g <= h )
assume h in X ; :: thesis: g <= h
then A7: ( h >= inf X & h . i in pi X,i ) by A2, CARD_3:def 6, LATTICE3:def 8;

now

let j be Element of I; :: thesis: h . j >= g . j
( g . j = (inf X) . j or ( g . j = x & j = i ) ) by A6, FUNCT_7:34;
hence h . j >= g . j by A4, A7, LATTICE3:def 8, WAYBEL_3:28; :: thesis: verum

end;

hence g <= h by WAYBEL_3:28; :: thesis: verum

end;

then inf X >= g by A1, YELLOW_0:31;
hence (inf X) . i >= x by A6, WAYBEL_3:28; :: thesis: verum

end;

hence ex_inf_of pi X,i,J . i by A3, YELLOW_0:31; :: thesis: verum

end;

assume for i being Element of I holds ex_inf_of pi X,i,J . i ; :: thesis: ex_inf_of X, product J
then consider f being Element of (product J) such that
for i being Element of I holds f . i = inf (pi X,i) and
A8: f is_<=_than X and
A9: for g being Element of (product J) st X is_>=_than g holds
f >= g by Lm2;
thus ex_inf_of X, product J by A8, A9, YELLOW_0:31; :: thesis: verum