let x, y be Nat; :: thesis: ( x > 1 & y > 1 implies x * y >= x + y )
assume A1: ( x > 1 & y > 1 ) ; :: thesis: x * y >= x + y

per cases ( x >= y or x < y ) ;

suppose A2: x >= y ; :: thesis: x * y >= x + y

y - 0 > 1 by A1;
then y - 1 >= 0 + 1 by INT_1:7, XREAL_1:12;
then x * (y - 1) >= y * 1 by A2, XREAL_1:66;
then ((x * y) - x) + x >= y + x by XREAL_1:6;
hence x * y >= x + y ; :: thesis: verum

end;

suppose A3: x < y ; :: thesis: x * y >= x + y

x - 0 > 1 by A1;
then x - 1 >= 0 + 1 by XREAL_1:12, INT_1:7;
then y * (x - 1) >= x * 1 by A3, XREAL_1:66;
then ((x * y) - y) + y >= x + y by XREAL_1:6;
hence x * y >= x + y ; :: thesis: verum

end;

end;