take {} T ; :: thesis: ( {} T is property(S) & {} T is closed_under_directed_sups )
thus ( {} T is property(S) & {} T is closed_under_directed_sups ) ; :: thesis: verum