take <%0_No%> ; :: thesis: <%0_No%> is uniq-surreal-valued
thus <%0_No%> is uniq-surreal-valued ; :: thesis: verum