let x, y be Real; :: thesis: ( y >= 0 & x >= 1 implies (x - 1) / y >= 0 )
assume that
A1: y >= 0 and
A2: x >= 1 ; :: thesis: (x - 1) / y >= 0
x + (- 1) >= 1 + (- 1) by A2, XREAL_1:6;
hence (x - 1) / y >= 0 by A1; :: thesis: verum