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

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

let x be Element of X; :: thesis: ex_sup_of pi A,x,(X --> L) . x
A1: (X --> L) . x = L by FUNCOP_1:13;
( pi B,x is directed & not pi B,x is empty ) by Th37;
hence ex_sup_of pi A,x,(X --> L) . x by A1, WAYBEL_0:75; :: thesis: verum

end;

hence ex_sup_of A,L |^ X by Th33; :: thesis: verum

end;

hence L |^ X is up-complete by WAYBEL_0:75; :: thesis: verum