theorem Th1: :: LIOUVIL1:1

for x, y being Nat st x > 1 & y > 1 holds
x * y >= x + y