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