thus [#] T is closed_under_directed_sups :: thesis: [#] T is inaccessible_by_directed_joins

proof

let D be non empty directed Subset of T; :: according to WAYBEL11:def 2 :: thesis: ( D c= [#] T implies sup D in [#] T )
assume D c= [#] T ; :: thesis: sup D in [#] T
thus sup D in [#] T ; :: thesis: verum

end;

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