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