let D be non empty directed Subset of T; :: according to WAYBEL11:def 2 :: thesis: ( D c= S ` implies sup D in S ` )
assume D c= S ` ; :: thesis: sup D in S `
then D misses S by SUBSET_1:23;
then not sup D in S by Def1;
hence sup D in S ` by XBOOLE_0:def 5; :: thesis: verum