for D being non empty directed Subset of T st sup D in {} T holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in {} T ) ) ;
hence {} T is property(S) by Def3; :: thesis: {} T is closed_under_directed_sups
thus for D being non empty directed Subset of T st D c= {} T holds
sup D in {} T ; :: according to WAYBEL11:def 2 :: thesis: verum