take [#] T ; :: thesis: ( not [#] T is empty & [#] T is dense )
thus ( not [#] T is empty & [#] T is dense ) ; :: thesis: verum