let i, j be Integer; :: thesis: ( i >= 0 & j >= 0 implies i div j >= 0 )
assume A1: ( i >= 0 & j >= 0 ) ; :: thesis: i div j >= 0
A2: (i / j) - 1 < [\(i / j)/] by Def4;
(i / j) - 1 >= 0 - 1 by A1, XREAL_1:11;
then - 1 < [\(i / j)/] by A2, XXREAL_0:2;
hence i div j >= 0 by Th21; :: thesis: verum