let S be Subset of T; :: thesis: ( S is empty implies ( S is property(S) & S is closed_under_directed_sups ) )
assume S is empty ; :: thesis: ( S is property(S) & S is closed_under_directed_sups )
then X: S = {} T ;
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 S is property(S) by X, Def3; :: thesis: S is closed_under_directed_sups
thus for D being non empty directed Subset of T st D c= S holds
sup D in S by X; :: according to WAYBEL11:def 2 :: thesis: verum