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_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi (X,i))
let J be non-Empty Poset-yielding ManySortedSet of I; for X being Subset of (product J) st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi (X,i))
let X be Subset of (product J); ( ex_sup_of X, product J implies for i being Element of I holds (sup X) . i = sup (pi (X,i)) )
assume
ex_sup_of X, product J
; for i being Element of I holds (sup X) . i = sup (pi (X,i))
then
for i being Element of I holds ex_sup_of pi (X,i),J . i
by Th30;
then consider f being Element of (product J) such that
A1:
for i being Element of I holds f . i = sup (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 Lm1;
sup X = f
by A2, A3, YELLOW_0:30;
hence
for i being Element of I holds (sup X) . i = sup (pi (X,i))
by A1; verum