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