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 positive

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

end;

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

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

end;

end;