let x, y be R_eal; :: thesis: ( ( ( 0 < x & y < 0 ) or ( x < 0 & 0 < y ) ) iff x * y < 0 )
( not x * y < 0 or ( 0 < x & y < 0 ) or ( x < 0 & 0 < y ) )

proof

assume A1: x * y < 0 ; :: thesis: ( ( 0 < x & y < 0 ) or ( x < 0 & 0 < y ) )
assume A2: ( not ( 0 < x & y < 0 ) & not ( x < 0 & 0 < y ) ) ; :: thesis: contradiction

per cases ( ( x <= 0 & 0 <= x ) or ( x <= 0 & y <= 0 ) or ( 0 <= x & 0 <= y ) or ( y <= 0 & 0 <= y ) ) by A2;

suppose ( x <= 0 & 0 <= x ) ; :: thesis: contradiction

then x = 0 ;
hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose A3: ( x <= 0 & y <= 0 ) ; :: thesis: contradiction

now

per cases ( x = 0 or x < 0 ) by A3;

suppose x = 0 ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose A4: x < 0 ; :: thesis: contradiction

now

per cases ( y = 0 or y < 0 ) by A3;

suppose y = 0 ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose y < 0 ; :: thesis: contradiction

hence contradiction by A1, A4, EXTREAL1:20; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A5: ( 0 <= x & 0 <= y ) ; :: thesis: contradiction

now

per cases ( x = 0 or 0 < x ) by A5;

suppose x = 0 ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose A6: 0 < x ; :: thesis: contradiction

now

per cases ( y = 0 or 0 < y ) by A5;

suppose y = 0 ; :: thesis: contradiction

hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

suppose 0 < y ; :: thesis: contradiction

hence contradiction by A1, A6, EXTREAL1:20; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose ( y <= 0 & 0 <= y ) ; :: thesis: contradiction

then y = 0 ;
hence contradiction by A1, EXTREAL1:def 1; :: thesis: verum

end;

end;

end;

hence ( ( ( 0 < x & y < 0 ) or ( x < 0 & 0 < y ) ) iff x * y < 0 ) by EXTREAL1:21; :: thesis: verum