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;
now :: thesis: for A being non empty directed Subset of (I -POS_prod J) holds ex_sup_of A,I -POS_prod J
let A be non empty directed Subset of (I -POS_prod J); :: thesis: ex_sup_of A,I -POS_prod J
now :: thesis: for x being Element of I holds ex_sup_of pi (A,x),J . x
let 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;
hence ex_sup_of A,I -POS_prod J by YELLOW16:31; :: thesis: verum
end;
hence I -POS_prod J is up-complete by WAYBEL_0:75; :: thesis: verum