per cases ( ( x is real & y is real ) or not x is real or not y is real ) ;

suppose ( x is real & y is real ) ; :: thesis: not x * y is zero

then reconsider r = x, s = y as Real ;
assume x * y is zero ; :: thesis: contradiction
then r * s = 0 ;
hence contradiction ; :: thesis: verum

end;

suppose ( not x is real or not y is real ) ; :: thesis: not x * y is zero

then x * y <> 0 by Lm18;
hence not x * y is zero ; :: thesis: verum

end;

end;