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