theorem :: XREAL_1:163

for a, b being Real st a <= - 1 & b <= - 1 holds
1 <= a * b