let I be non empty set ; for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ex_inf_of X, product J holds
for i being Element of I holds (inf X) . i = inf (pi (X,i))
let J be non-Empty Poset-yielding ManySortedSet of I; for X being Subset of (product J) st ex_inf_of X, product J holds
for i being Element of I holds (inf X) . i = inf (pi (X,i))
let X be Subset of (product J); ( ex_inf_of X, product J implies for i being Element of I holds (inf X) . i = inf (pi (X,i)) )
assume
ex_inf_of X, product J
; for i being Element of I holds (inf X) . i = inf (pi (X,i))
then
for i being Element of I holds ex_inf_of pi (X,i),J . i
by Th31;
then consider f being Element of (product J) such that
A1:
for i being Element of I holds f . i = inf (pi (X,i))
and
A2:
f is_<=_than X
and
A3:
for g being Element of (product J) st X is_>=_than g holds
f >= g
by Lm2;
inf X = f
by A2, A3, YELLOW_0:31;
hence
for i being Element of I holds (inf X) . i = inf (pi (X,i))
by A1; verum