let i, j be Integer; :: thesis: ( i >= 0 & j >= 0 implies i div j >= 0 )
assume that
A1: i >= 0 and
A2: j >= 0 ; :: thesis: i div j >= 0
A3: (i / j) - 1 < [\(i / j)/] by Def6;
(i / j) - 1 >= 0 - 1 by A1, A2, XREAL_1:9;
then - 1 < [\(i / j)/] by A3, XXREAL_0:2;
hence i div j >= 0 by Th8; :: thesis: verum