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