take <% the object %> ; :: thesis: ( not <% the object %> is empty & <% the object %> is trivial )
thus ( not <% the object %> is empty & <% the object %> is trivial ) ; :: thesis: verum