per cases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ;

suppose ( x in REAL & y in REAL ) ; :: thesis: x * y is negative

then reconsider x = x, y = y as Real ;
x * y < 0 ;
hence x * y is negative ; :: thesis: verum

end;

suppose ( not x in REAL or not y in REAL ) ; :: thesis: x * y is negative

then ( not x is real or not y is real ) by XREAL_0:def 1;
hence x * y is negative by Def5; :: thesis: verum

end;

end;