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;