let I be non empty set ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum