thus [#] T is directly_closed ; :: thesis: [#] T is inaccessible_by_directed_joins
let D be non empty directed Subset of T; :: according to WAYBEL11:def 1 :: thesis: ( sup D in [#] T implies D meets [#] T )
assume sup D in [#] T ; :: thesis: D meets [#] T
ex p being Element of T st p in D by SUBSET_1:4;
hence D meets [#] T by XBOOLE_0:3; :: thesis: verum