take <% the non empty set %> ; :: thesis: <% the non empty set %> is non-empty
thus <% the non empty set %> is non-empty ; :: thesis: verum