let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis:
assume A3: sup D in S ; :: thesis:
S is inaccessible by A1, Def4;
then S meets D by A3;
then consider y being object such that
A4: y in S and
A5: y in D by XBOOLE_0:3;
reconsider y = y as Element of T by A4;
take y ; :: thesis:
thus ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) by A2, A4, A5; :: thesis:

end;

let D be non empty directed Subset of T; :: according to WAYBEL11:def 1 :: thesis:
assume sup D in S ; :: thesis:
then consider y being Element of T such that
A8: y in D and
A9: for x being Element of T st x in D & x >= y holds
x in S by A7;
y >= y by YELLOW_0:def 1;
then y in S by A8, A9;
hence D meets S by A8, XBOOLE_0:3; :: thesis:

end;