( 0_No < x & 0_No < y ) by Def8;
hence x * y is positive by SURREALR:72; :: thesis: verum