let x, y be ext-real number ; :: thesis: ( not x is real & x * y = 0 implies y = 0 )
assume that
Z1: not x is real and
Z2: x * y = 0 ; :: thesis: y = 0
( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) by Z2;
hence y = 0 by Z1, Z2; :: thesis: verum