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