let X be non empty set ; :: thesis: for L being non empty up-complete Poset holds L |^ X is up-complete
let L be non empty up-complete Poset; :: thesis: L |^ X is up-complete
now :: thesis: for A being non empty directed Subset of (L |^ X) holds ex_sup_of A,L |^ X
let A be non empty directed Subset of (L |^ X); :: thesis: ex_sup_of A,L |^ X
reconsider B = A as non empty directed Subset of (product (X --> L)) ;
now :: thesis: for x being Element of X holds ex_sup_of pi (A,x),(X --> L) . x
let x be Element of X; :: thesis: ex_sup_of pi (A,x),(X --> L) . x
( pi (B,x) is directed & not pi (B,x) is empty ) by Th34;
hence ex_sup_of pi (A,x),(X --> L) . x by WAYBEL_0:75; :: thesis: verum
end;
hence ex_sup_of A,L |^ X by Th30; :: thesis: verum
end;
hence L |^ X is up-complete by WAYBEL_0:75; :: thesis: verum