theorem Lm3: :: SURREALI:41

for x, y being Surreal holds
( x * y == 0_No iff ( x == 0_No or y == 0_No ) ) by SURREALR:72, SURREALR:74;