take <%1,1%> ; :: thesis: ( not <%1,1%> is empty & not <%1,1%> is trivial & <%1,1%> is non-empty & <%1,1%> is finite & <%1,1%> is with_cardinal_domain & <%1,1%> is Cardinal-yielding )
thus ( not <%1,1%> is empty & not <%1,1%> is trivial & <%1,1%> is non-empty & <%1,1%> is finite & <%1,1%> is with_cardinal_domain & <%1,1%> is Cardinal-yielding ) ; :: thesis: verum