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 & d is_>=_than D ) by WAYBEL_0:1;
A2: ex_sup_of D,L by WAYBEL_0:75;
then sup D is_>=_than D by YELLOW_0:30;
then ( sup D <= d & sup D >= d ) by A1, A2, LATTICE3:def 9, YELLOW_0:30;
hence sup D in D by A1, ORDERS_2:25; :: thesis: verum