take <%1%> ; :: thesis: ( not <%1%> is empty & <%1%> is non-empty & <%1%> is natural-valued )
thus ( not <%1%> is empty & <%1%> is non-empty & <%1%> is natural-valued ) ; :: thesis: verum