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 Th34;
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