let I be non empty set ; :: thesis: for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds

I -POS_prod J is up-complete

let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is up-complete ) implies I -POS_prod J is up-complete )

assume A1: for i being Element of I holds J . i is up-complete ; :: thesis: I -POS_prod J is up-complete

set L = I -POS_prod J;

I -POS_prod J is up-complete

let J be non-Empty Poset-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is up-complete ) implies I -POS_prod J is up-complete )

assume A1: for i being Element of I holds J . i is up-complete ; :: thesis: I -POS_prod J is up-complete

set L = I -POS_prod J;

now :: thesis: for A being non empty directed Subset of (I -POS_prod J) holds ex_sup_of A,I -POS_prod J

hence
I -POS_prod J is up-complete
by WAYBEL_0:75; :: thesis: verumlet A be non empty directed Subset of (I -POS_prod J); :: thesis: ex_sup_of A,I -POS_prod J

end;now :: thesis: for x being Element of I holds ex_sup_of pi (A,x),J . x

hence
ex_sup_of A,I -POS_prod J
by YELLOW16:31; :: thesis: verumlet x be Element of I; :: thesis: ex_sup_of pi (A,x),J . x

( J . x is non empty up-complete Poset & pi (A,x) is directed & not pi (A,x) is empty ) by A1, YELLOW16:35;

hence ex_sup_of pi (A,x),J . x by WAYBEL_0:75; :: thesis: verum

end;( J . x is non empty up-complete Poset & pi (A,x) is directed & not pi (A,x) is empty ) by A1, YELLOW16:35;

hence ex_sup_of pi (A,x),J . x by WAYBEL_0:75; :: thesis: verum