let S be Subset of T; :: thesis: S is inaccessible
let D be non empty directed Subset of T; :: according to WAYBEL11:def 1 :: thesis: ( sup D in S implies D meets S )
assume A1: sup D in S ; :: thesis: D meets S
sup D in D by Th4;
hence D meets S by A1, XBOOLE_0:3; :: thesis: verum