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;