let L be non empty up-complete Poset; :: thesis: for D being non empty finite directed Subset of L holds sup D in D
let D be non empty finite directed Subset of L; :: thesis: sup D in D
D c= D ;
then consider d being Element of L such that
A1: d in D and
A2: d is_>=_than D by WAYBEL_0:1;
A3: ex_sup_of D,L by WAYBEL_0:75;
then A4: sup D is_>=_than D by YELLOW_0:30;
A5: sup D <= d by A2, A3, YELLOW_0:30;
sup D >= d by A1, A4;
hence sup D in D by A1, A5, ORDERS_2:2; :: thesis: verum