let x, y be Surreal; :: thesis: ( 0_No < x & 0_No < y implies 0_No < x * y )
assume ( 0_No < x & 0_No < y ) ; :: thesis: 0_No < x * y
then (0_No * y) + (x * 0_No) < (0_No * 0_No) + (x * y) by Th51;
hence 0_No < x * y ; :: thesis: verum