let D be non empty directed Subset of T; :: according to WAYBEL11:def 2 :: thesis: ( D c= S ` implies sup D in S ` )
assume A1: D c= S ` ; :: thesis: sup D in S `
assume not sup D in S ` ; :: thesis: contradiction
then sup D in S by XBOOLE_0:def 5;
then consider y being Element of T such that
A2: y in D and
A3: for x being Element of T st x in D & x >= y holds
x in S by Def3;
y <= y ;
then y in S by A2, A3;
then D /\ S <> {} by A2, XBOOLE_0:def 4;
then D meets S ;
hence contradiction by A1, SUBSET_1:23; :: thesis: verum