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