let y, x be real number ; :: thesis: ( y >= 0 & x >= 1 implies (x - 1) / y >= 0 )
assume A1: ( y >= 0 & x >= 1 ) ; :: thesis: (x - 1) / y >= 0
then x + (- 1) >= 1 + (- 1) by XREAL_1:8;
hence (x - 1) / y >= 0 by A1; :: thesis: verum