take [#] T ; :: thesis: ( [#] T is closed_under_directed_sups & [#] T is lower & [#] T is inaccessible_by_directed_joins & [#] T is upper )
thus ( [#] T is closed_under_directed_sups & [#] T is lower & [#] T is inaccessible_by_directed_joins & [#] T is upper ) ; :: thesis: verum