take {0_No} ; :: thesis: ( not {0_No} is empty & {0_No} is surreal-membered )
thus ( not {0_No} is empty & {0_No} is surreal-membered ) ; :: thesis: verum