( 0_No < x & 0_No <= y ) by Def8;
then 0_No + 0_No < x + y by SURREALR:44;
hence x + y is positive ; :: thesis: verum