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